pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-20 04:07:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Finish port to Coq 8.6

Browse source
This commit is contained in:
Adam Chlipala 2017-02-07 20:51:13 -05:00
parent 1768aa6ea7
commit 466ea72b27
3 changed files with 15 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
Frap.v
View file

@ -69,10 +69,13 @@ Ltac same_structure x y :=
Ltac instantiate_obvious1 H := Ltac instantiate_obvious1 H :=
match type of H with match type of H with
| _ ++ _ = _ ++ _ -> _ => fail 1
| ?x = ?y -> _ => | ?x = ?y -> _ =>
(same_structure x y; specialize (H eq_refl)) || fail 3 (same_structure x y; specialize (H eq_refl))
|| (has_evar (x, y); fail 3)
| JMeq.JMeq ?x ?y -> _ => | JMeq.JMeq ?x ?y -> _ =>
(same_structure x y; specialize (H JMeq.JMeq_refl)) || fail 3 (same_structure x y; specialize (H JMeq.JMeq_refl))
|| (has_evar (x, y); fail 3)
| forall x : ?T, _ => | forall x : ?T, _ =>
match type of T with match type of T with
| Prop => fail 1 | Prop => fail 1

5
SharedMemory.v
View file

@ -1496,6 +1496,7 @@ Proof.
cases r1; simplify; subst. cases r1; simplify; subst.
right; eexists (_ :: _); simplify; eauto. right; eexists (_ :: _); simplify; eauto.
invert H. invert H.
first_order; subst; eauto.
apply IHl1 in H2; first_order; subst; eauto. apply IHl1 in H2; first_order; subst; eauto.
Qed. Qed.
@ -1550,7 +1551,7 @@ Proof.
cases x3; simplify. cases x3; simplify.
invert H. invert H.
eapply nextAction_det in H0; eauto; propositional; subst. eapply nextAction_det in H0; try eapply H5; eauto; propositional; subst.
eauto 10. eauto 10.
invert H. invert H.
@ -1574,7 +1575,7 @@ Proof.
cases x3; simplify. cases x3; simplify.
invert H. invert H.
eapply nextAction_det in H0; eauto; propositional; subst. eapply nextAction_det in H0; try eapply H5; eauto; propositional; subst.
eauto 10. eauto 10.
invert H. invert H.

9
TypesAndMutation.v
View file

@ -236,6 +236,7 @@ Module References.
| [ H : step _ _ |- _ ] => invert H | [ H : step _ _ |- _ ] => invert H
end; end;
repeat match goal with repeat match goal with
| [ H : plug _ _ _ |- _ ] => invert1 H
| [ H : plug _ _ _ |- _ ] => invert H | [ H : plug _ _ _ |- _ ] => invert H
| [ H : step0 _ _ |- _ ] => invert1 H | [ H : step0 _ _ |- _ ] => invert1 H
| [ H : value _ |- _ ] => invert1 H | [ H : value _ |- _ ] => invert1 H
@ -302,8 +303,12 @@ Module References.
\/ exists he', step (h, e) he'. \/ exists he', step (h, e) he'.
Proof. Proof.
induct 2; t. induct 2; t.
apply H2 in H8; t. match goal with
apply H1 in H8; t. | [ H1 : _ = Some _, H2 : forall l : loc, _ |- _ ] => apply H3 in H8; t
end.
match goal with
| [ H1 : _ = Some _, H2 : forall l : loc, _ |- _ ] => apply H3 in H8; t
end.
Qed. Qed.
(* Now, a series of lemmas essentially copied from original type-soundness (* Now, a series of lemmas essentially copied from original type-soundness