vafeiadis / hahn Goto Github PK
View Code? Open in Web Editor NEWHahn: A Coq library
License: MIT License
Hahn: A Coq library
License: MIT License
In the following code, desc
terminates in the proof of ff
but doesn't in the proof of ff'
.
From hahn Require Import Hahn.
Theorem ff (HH : << AA : True >> /\ << BB : True >>) : False.
Proof.
desc.
Admitted.
Section aa.
Variable HH : << AA : True >> /\ << BB : True >>.
Theorem ff' : False.
Proof.
desc.
Admitted.
End aa.
The same problem is presented if we replace desc
with its part:
repeat match goal with
| H : ?p /\ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => red in x' | _ => idtac end;
match q with | NW _ => red in y' | _ => idtac end
end.
That is, the problem appears since destruct HH
doesn't remove HH
from hypotheses if HH
is a section variable.
Replacing destruct H as [x' y']
with destruct H as [x' y']; clear H
in the tactic solves the problem.
I propose to update the des*
family of tactics in that way.
Installation from opam on Coq 8.9.1 fails on building HahnCountable. The problem is due to the seq_app
lemma which seems to be added later.
Also, it's unclear to me how opam resolves version requirements because currently opam configuration file states that Coq version should be less than 8.9. However, this check only occurs on attempt to pin hahn to another repository and not on regular opam upgrade
. Also, there are commit messages saying that hahn works on 8.10 as well.
From hahn Require Import Hahn.
Section aa.
Variables A B C D : Prop.
Hypothesis HH : A /\ B.
Lemma aaa (OO : C \/ D) : False.
Proof.
desf.
Admitted.
End aa.
In the code above, desf
doesn't destruct OO. However, if you put clear HH
before desf
, then it does.
This is not an actual "issue", but rather a question about the design of the library.
I am a bit confused about the relationship between (co)dom_rel
and doma
/domb
.
dom_rel
is defined in HahnRelationsBasic.v
as follows:
Definition dom_rel := fun x => exists y, r x y.
doma
is defined in HahnDom.v
as follows:
Definition doma := forall x y (REL: r x y), d x.
Clearly there is a connection between the two.
If we fix relation r
then all sets d
satisfying doma r d
will form partially ordered set (ordered by set inclusion) with dom_rel r
as a minimal element.
However, I cannot find any lemma in Hahn
that relate these two definitions (please, correct me if I am wrong). Moreover some lemmas about doma
duplicate similar lemmas for dom_rel
.
For example
Lemma doma_rewrite : doma r d -> r ⊆ ⦗d⦘ ⨾ r.
and
Lemma dom_rel_helper (IN : dom_rel r ⊆₁ d) : r ≡ ⦗d⦘ ⨾ r.
So my question is what doma
/domb
are useful for?
Are they more convenient to work with in some situations compared to dom_rel
/codom_rel
?
Why there are no lemmas relating the two?
BTW, just grep
ed in weakestmoToImm
and IMM
repos.
It seems that doma
/domb
are not used in weakestmo
at all (except two usages related to IMM),
and used rarely in IMM
(and I suppose all these usages can be refactored to use dom_rel
instead).
Goal forall a b c d e f g h i : relation actid, a ⨾ b ⨾ c ⨾ d ⨾ e ⨾ f ⨾ g ⨾ h ⨾ i ⊆ ∅₂.
Proof.
intros.
arewrite (a ⨾ b ⨾ c ⨾ d ⨾ e ⨾ f ⨾ g ⨾ h ⊆ ∅₂).
fails. Am I doing something wrong or did I reach some internal limit of sin_rewrite etc?
Lemma plain_coherence_helper (r s t : relation actid) : r ∩ s⁻¹ ∪ t ≡ ∅₂ -> irreflexive (s ⨾ r).
Proof.
basic_solver 42.
gives me
All the remaining goals are on the shelf:
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
actid
It seems some lemmas are incompatible with 8.15.1, or something is wrong on my end.
The problems are in HahnMinPath and HahnWf.
the problem in HahnWf seems to be related to a mismatch between the internal name of the binder (y) and what is shown on screen (y0). It can be fixed like this:
rename y into y'. (* not necessary, but makes sure that the names stay the same *)
apply In_split in IN; desf.
eapply H with (y := l1 ++ l2); ins. (* was y0:= *)
by rewrite !app_length; simpl; lia.
However it's strange that the names are not the same and could point to the problem being in my installation.
Dear Viktor,
I am migrating the promising semantics Coq model (https://github.com/snu-sf/promising-coq) from Coq 8.5 to 8.6. As it depends on hahn, I wonder if you have a plan to migrate hahn to 8.6. I tried myself but I couldn't leave the proof style untouched, and cannot help making the proof longer..
It seems that the index given to the LTS_final
predicate is incorrect in HahnTrace, line 733.
If I am not mistaken, LTS_final
is used to denote the terminal state. However LTS_complete_trace
requires state 0
to be terminal. It is not obvious why it should be this way.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.