Skip to content

Commit

Permalink
update for Coq 8.11
Browse files Browse the repository at this point in the history
  • Loading branch information
garrigue committed Apr 8, 2020
1 parent 5061c37 commit 780cdef
Show file tree
Hide file tree
Showing 8 changed files with 48 additions and 49 deletions.
10 changes: 6 additions & 4 deletions Cardinal.v
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ Proof.
inversion H3.
destruct (S.E.compare a a0).
elim (sort_lt_notin H1 (cons_leA _ _ _ _ l1)).
apply* (proj1 (H2 a)).
apply* (proj1 (H2 a)). auto with ordered_type.
rewrite <- e in *. clear e a0.
rewrite* (IHSorted l0).
intro; split; intro.
Expand All @@ -71,7 +71,7 @@ Proof.
use (proj2 (H2 a0) (InA_cons_tl a H5)).
inversions* H6.
elim (sort_lt_notin (cons_sort H H0) (cons_leA _ _ _ _ l1)).
apply* (proj2 (H2 a0)).
apply* (proj2 (H2 a0)). auto with ordered_type.
Qed.

Lemma remove_union : forall a L1 L2,
Expand Down Expand Up @@ -226,7 +226,7 @@ Proof.
apply S.elements_1.
apply* S.remove_2.
apply S.elements_2.
rewrite* <- Heqelts.
rewrite* <- Heqelts. auto with ordered_type.
inversions H. elim n0; auto.
eauto with sets.
rewrite* <- (@elements_tl a0 elts L).
Expand All @@ -250,6 +250,7 @@ Proof.
assert (a \in L2).
apply S.elements_2.
rewrite* <- Heqelts2.
auto with ordered_type.
assert (InA S.E.eq a elts).
subst.
auto with sets.
Expand Down Expand Up @@ -343,6 +344,7 @@ Proof.
apply H.
apply S.elements_2.
rewrite* <- Heqelts1.
auto with ordered_type.
rewrite <- (cardinal_remove H3).
omega.
Qed.
Expand All @@ -353,7 +355,7 @@ Proof.
case_eq (S.elements {}); intros. simpl*.
assert (In e (e::l)) by auto.
rewrite <- H in H0.
assert (e \in {}). auto with sets.
assert (e \in {}). auto with sets ordered_type.
elim (in_empty H1).
Qed.

Expand Down
1 change: 1 addition & 0 deletions Extraction.v
Original file line number Diff line number Diff line change
Expand Up @@ -155,5 +155,6 @@ Definition eval1 fenv t h := eval fenv h nil nil t nil.

(* Export and try to do this in ocaml *)
Require Import Extraction.
(* Extraction Language Haskell. *)
Set Extraction AccessOpaque.
Extraction "typinf" typinf1 eval1.
64 changes: 32 additions & 32 deletions FSetList.v
Original file line number Diff line number Diff line change
Expand Up @@ -252,10 +252,10 @@ Module Raw (X: OrderedType).
Lemma add_1 :
forall (s : t) (Hs : Sort s) (x y : elt), X.eq x y -> In y (add x s).
Proof.
simple induction s.
simple induction s.
simpl; intuition.
simpl; intros; case (X.compare x a); inversion_clear Hs; auto.
constructor; apply X.eq_trans with x; auto.
simpl; intros; case (X.compare x a); inversion_clear Hs; auto with ordered_type.
constructor; apply X.eq_trans with x; auto with ordered_type.
Qed.

Lemma add_2 :
Expand Down Expand Up @@ -320,7 +320,7 @@ Module Raw (X: OrderedType).
simpl; intuition.
simpl; intros; case (X.compare x a); intuition; inversion_clear Hs;
inversion_clear H1; auto.
destruct H0; apply X.eq_trans with a; auto.
destruct H0; apply X.eq_trans with a; auto with ordered_type.
Qed.

Lemma remove_3 :
Expand All @@ -341,12 +341,12 @@ Module Raw (X: OrderedType).
Lemma singleton_1 : forall x y : elt, In y (singleton x) -> X.eq x y.
Proof.
unfold singleton; simpl; intuition.
inversion_clear H; auto; inversion H0.
inversion_clear H; auto with ordered_type; inversion H0.
Qed.

Lemma singleton_2 : forall x y : elt, X.eq x y -> In y (singleton x).
Proof.
unfold singleton; simpl; auto.
unfold singleton; simpl; auto with ordered_type.
Qed.

Ltac DoubleInd :=
Expand All @@ -371,8 +371,8 @@ Module Raw (X: OrderedType).
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), Sort (union s s').
Proof.
DoubleInd; case (X.compare x x'); intuition; constructor; auto.
apply Inf_eq with x'; trivial; apply union_Inf; trivial; apply Inf_eq with x; auto.
change (Inf x' (union (x :: l) l')); auto.
apply Inf_eq with x'; trivial; apply union_Inf; trivial; apply Inf_eq with x; auto with ordered_type.
change (Inf x' (union (x :: l) l')); auto with ordered_type.
Qed.

Lemma union_1 :
Expand All @@ -399,7 +399,7 @@ Module Raw (X: OrderedType).
Proof.
DoubleInd.
intros i Hi; case (X.compare x x'); inversion_clear Hi; intuition.
constructor; apply X.eq_trans with x'; auto.
constructor; apply X.eq_trans with x'; auto with ordered_type.
Qed.

Lemma inter_Inf :
Expand All @@ -420,7 +420,7 @@ Module Raw (X: OrderedType).
Proof.
DoubleInd; case (X.compare x x'); auto.
constructor; auto.
apply Inf_eq with x'; trivial; apply inter_Inf; trivial; apply Inf_eq with x; auto.
apply Inf_eq with x'; trivial; apply inter_Inf; trivial; apply Inf_eq with x; auto with ordered_type.
Qed.

Lemma inter_1 :
Expand Down Expand Up @@ -453,7 +453,7 @@ Module Raw (X: OrderedType).
generalize (Sort_Inf_In Hs' (cons_leA _ _ _ _ l0) His'); order.

inversion_clear His; auto; inversion_clear His'; auto.
constructor; apply X.eq_trans with x'; auto.
constructor; apply X.eq_trans with x'; auto with ordered_type.

change (In i (inter (x :: l) l')).
inversion_clear His'; auto.
Expand Down Expand Up @@ -528,15 +528,15 @@ Module Raw (X: OrderedType).
simple induction s; unfold Equal.
intro s'; case s'; auto.
simpl; intuition.
elim (H e); intros; assert (A : In e nil); auto; inversion A.
elim (H e); intros; assert (A : In e nil); auto with ordered_type; inversion A.
intros x l Hrec s'.
case s'.
intros; elim (H x); intros; assert (A : In x nil); auto; inversion A.
intros; elim (H x); intros; assert (A : In x nil); auto with ordered_type; inversion A.
intros x' l' Hs Hs'; inversion Hs; inversion Hs'; subst.
simpl; case (X.compare x); intros; auto.

elim (H x); intros.
assert (A : In x (x' :: l')); auto; inversion_clear A.
assert (A : In x (x' :: l')); auto with ordered_type; inversion_clear A.
order.
generalize (Sort_Inf_In H5 H6 H4); order.

Expand All @@ -547,7 +547,7 @@ Module Raw (X: OrderedType).
generalize (Sort_Inf_In H5 H6 H0); order.

elim (H x'); intros.
assert (A : In x' (x :: l)); auto; inversion_clear A.
assert (A : In x' (x :: l)); auto with ordered_type; inversion_clear A.
order.
generalize (Sort_Inf_In H1 H2 H4); order.
Qed.
Expand All @@ -564,8 +564,8 @@ Module Raw (X: OrderedType).
intros x' l'; simpl; case (X.compare x); intros; auto; try discriminate.
elim (Hrec l' H a); intuition; inversion_clear H2; auto.
constructor; apply X.eq_trans with x; auto.
constructor; apply X.eq_trans with x'; auto.
Qed.
constructor; apply X.eq_trans with x'; auto with ordered_type.
Qed.

Lemma subset_1 :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'),
Expand All @@ -574,13 +574,13 @@ Module Raw (X: OrderedType).
intros s s'; generalize s' s; clear s s'.
simple induction s'; unfold Subset.
intro s; case s; auto.
intros; elim (H e); intros; assert (A : In e nil); auto; inversion A.
intros; elim (H e); intros; assert (A : In e nil); auto with ordered_type; inversion A.
intros x' l' Hrec s; case s.
simpl; auto.
intros x l Hs Hs'; inversion Hs; inversion Hs'; subst.
simpl; case (X.compare x); intros; auto.

assert (A : In x (x' :: l')); auto; inversion_clear A.
assert (A : In x (x' :: l')); auto with ordered_type; inversion_clear A.
order.
generalize (Sort_Inf_In H5 H6 H0); order.

Expand Down Expand Up @@ -624,7 +624,7 @@ Module Raw (X: OrderedType).
Lemma is_empty_1 : forall s : t, Empty s -> is_empty s = true.
Proof.
unfold Empty; intro s; case s; simpl; intuition.
elim (H e); auto.
elim (H e); auto with ordered_type.
Qed.

Lemma is_empty_2 : forall s : t, is_empty s = true -> Empty s.
Expand All @@ -650,12 +650,12 @@ Module Raw (X: OrderedType).

Lemma elements_3w : forall (s : t) (Hs : Sort s), NoDupA X.eq (elements s).
Proof.
unfold elements; auto.
unfold elements; auto with ordered_type.
Qed.

Lemma min_elt_1 : forall (s : t) (x : elt), min_elt s = Some x -> In x s.
Proof.
intro s; case s; simpl; intros; inversion H; auto.
intro s; case s; simpl; intros; inversion H; auto with ordered_type.
Qed.

Lemma min_elt_2 :
Expand Down Expand Up @@ -685,7 +685,7 @@ Module Raw (X: OrderedType).
intros; inversion H.
intros x l; case l; simpl.
intuition.
inversion H0; auto.
inversion H0; auto with ordered_type.
intros.
constructor 2; apply (H _ H0).
Qed.
Expand All @@ -703,7 +703,7 @@ Module Raw (X: OrderedType).
order.
inversion H3.
intros; inversion_clear Hs; inversion_clear H3; inversion_clear H1.
assert (In e (e::l0)) by auto.
assert (In e (e::l0)) by auto with ordered_type.
generalize (H H2 x0 e H0 H1); order.
generalize (H H2 x0 y H0 H3); order.
Qed.
Expand All @@ -714,7 +714,7 @@ Module Raw (X: OrderedType).
red; intros; inversion H0.
intros x l; case l; simpl; intros.
inversion H0.
elim (H H0 e); auto.
elim (H H0 e); auto with ordered_type.
Qed.

Definition choose_1 :
Expand Down Expand Up @@ -800,7 +800,7 @@ Module Raw (X: OrderedType).
intros x l Hrec a f Hf.
generalize (Hf x); case (f x); simpl; auto.
inversion_clear 2; auto.
symmetry; auto.
symmetry; auto with ordered_type.
Qed.

Lemma filter_3 :
Expand All @@ -825,7 +825,7 @@ Module Raw (X: OrderedType).
intros x l Hrec f Hf.
generalize (Hf x); case (f x); simpl.
auto.
intros; rewrite (H x); auto.
intros; rewrite (H x); auto with ordered_type.
Qed.

Lemma for_all_2 :
Expand Down Expand Up @@ -870,7 +870,7 @@ Module Raw (X: OrderedType).
intros; discriminate.
intros x l Hrec f Hf.
case_eq (f x); intros.
exists x; auto.
exists x; auto with ordered_type.
destruct (Hrec f Hf H0) as [a (A1,A2)].
exists a; auto.
Qed.
Expand Down Expand Up @@ -997,10 +997,10 @@ Module Raw (X: OrderedType).
unfold eq, Equal.
intros s s' Hs Hs' H; generalize Hs Hs'; clear Hs Hs'; elim H; intros; intro.
elim (H0 x); intros.
assert (X : In x nil); auto; inversion X.
assert (X : In x nil); auto with ordered_type; inversion X.
inversion_clear Hs; inversion_clear Hs'.
elim (H1 x); intros.
assert (X : In x (y :: s'0)); auto; inversion_clear X.
assert (X : In x (y :: s'0)); auto with ordered_type; inversion_clear X.
order.
generalize (Sort_Inf_In H4 H5 H8); order.
inversion_clear Hs; inversion_clear Hs'.
Expand Down Expand Up @@ -1031,11 +1031,11 @@ Module Raw (X: OrderedType).
| constructor 2
| constructor 3
| inversion Hs
| inversion Hs' ]; auto.
| inversion Hs' ]; auto with ordered_type.
generalize e; unfold eq, Equal; intuition; inversion_clear H.
constructor; apply X.eq_trans with a; auto.
destruct (e1 a0); auto.
constructor; apply X.eq_trans with a'; auto.
constructor; apply X.eq_trans with a'; auto with ordered_type.
destruct (e1 a0); auto.
Defined.

Expand Down
4 changes: 2 additions & 2 deletions ML_SP_Inference.v
Original file line number Diff line number Diff line change
Expand Up @@ -1146,7 +1146,7 @@ Proof.
elim (sort_lt_notin H0 H).
puts (mkset_in _ Hy').
clear -H1.
induction l; auto.
induction l; auto with ordered_type.
Qed.

Lemma typing_let_fresh : forall T1 l l0 K' e e0 e1 e2 fvT1 fvE,
Expand Down Expand Up @@ -2267,7 +2267,7 @@ Proof.
unfold vars_subst.
remember (S.elements {}) as l.
destruct* l.
assert (SetoidList.InA E.eq e (e::l)) by auto.
assert (SetoidList.InA E.eq e (e::l)) by auto with ordered_type.
rewrite Heql in H.
puts (S.elements_2 H). elim (in_empty H0).
Qed.
Expand Down
4 changes: 2 additions & 2 deletions ML_SP_Inference_wf.v
Original file line number Diff line number Diff line change
Expand Up @@ -1469,7 +1469,7 @@ Proof.
elim (sort_lt_notin H0 H).
puts (mkset_in _ Hy').
clear -H1.
induction l; auto.
induction l; auto with ordered_type.
Qed.

Lemma typing_let_fresh : forall T1 l l0 K' e e0 e1 e2 fvT1 fvE,
Expand Down Expand Up @@ -2566,7 +2566,7 @@ Proof.
unfold vars_subst.
remember (S.elements {}) as l.
destruct* l.
assert (SetoidList.InA E.eq e (e::l)) by auto.
assert (SetoidList.InA E.eq e (e::l)) by auto with ordered_type.
rewrite Heql in H.
puts (S.elements_2 H). elim (in_empty H0).
Qed.
Expand Down
4 changes: 2 additions & 2 deletions Metatheory_SP.v
Original file line number Diff line number Diff line change
Expand Up @@ -1281,9 +1281,9 @@ Proof.
rewrite <- Heql in H1.
inversions H1. inversions H5.
assert (e \in {{x}}). apply S.elements_2.
rewrite* <- Heql.
rewrite* <- Heql. auto with ordered_type.
assert (e0 \in {{x}}). apply S.elements_2.
rewrite* <- Heql.
rewrite* <- Heql. auto with ordered_type.
rewrite <- (S.singleton_1 H2) in H3.
rewrite <- (S.singleton_1 H6) in H3.
elim (E.lt_not_eq _ _ H3). reflexivity.
Expand Down
4 changes: 0 additions & 4 deletions Metatheory_Var.v
Original file line number Diff line number Diff line change
Expand Up @@ -69,8 +69,6 @@ Local Open Scope set_scope.

Definition vars := VarSet.S.t.

Import ZArith.

Lemma max_lt_l :
forall (x y z : Z), x <= y -> x <= Z.max y z.
Proof.
Expand Down Expand Up @@ -326,5 +324,3 @@ Tactic Notation "inst_notin" constr(lemma) constr(var)
Tactic Notation "inst_notin" "*" constr(lemma) constr(var)
"as" ident(hyp_name) :=
inst_notin lemma var as hyp_name; auto*.


6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
## A Certified Interpreter for ML with Structural Polymorphism
### Jacques Garrigue, updated November 2019
### Jacques Garrigue, updated April 2020

The files in this archive contain a proof of type soundness for structural
polymorphism based on local constraints [1], together with soundness
Expand Down Expand Up @@ -30,8 +30,8 @@ Of the above, Definitions, Infrastructure and Soundness are base on
the core ML proof, but were heavily modified.
Eval, Unify, Inference and Domain are completely new.

All the above development were checked with coq 8.10.1.
(Porting to 8.10.1 is the only change wrt. the version of september 2010)
All the above development were checked with coq 8.11.0.
(Porting to 8.11.0 is the only change wrt. the version of september 2010)
You can compile them with "sh build.sh"

You can also play with the type checker. It does not work inside Coq
Expand Down

0 comments on commit 780cdef

Please sign in to comment.