Commit 1f74a730 authored by Armaël Guéneau's avatar Armaël Guéneau

Make the library compatible with Coq 8.6.1 and newer

It seems the hsimpl tactic was in some cases working thanks to a bug in Ltac
pattern matching, introduced in Coq 8.4, and that was fixed in Coq
8.6.1 (https://github.com/coq/coq/issues/5487).

The fix implemented here makes hsimpl slightly more powerful in some cases, so
proofs may need to be updated.
parent e7e1c856
...@@ -1923,16 +1923,16 @@ Ltac hsimpl_try_same tt := ...@@ -1923,16 +1923,16 @@ Ltac hsimpl_try_same tt :=
Ltac hsimpl_find_same H HL := Ltac hsimpl_find_same H HL :=
match HL with match HL with
| H \* _ => apply hsimpl_cancel_1 | ?H' \* _ => unify H H'; apply hsimpl_cancel_1
| _ \* H \* _ => apply hsimpl_cancel_2 | _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_2
| _ \* _ \* H \* _ => apply hsimpl_cancel_3 | _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_3
| _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_4 | _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_4
| _ \* _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_5 | _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_5
| _ \* _ \* _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_6 | _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_6
| _ \* _ \* _ \* _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_7 | _ \* _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_7
| _ \* _ \* _ \* _ \* _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_8 | _ \* _ \* _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_8
| _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_9 | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_9
| _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_10 | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_10
end. end.
Ltac hsimpl_find_data l HL cont := Ltac hsimpl_find_data l HL cont :=
...@@ -2421,7 +2421,7 @@ Lemma Group_add : forall a (x:a) A `{Inhab A} (M:map a A) (G:htype A a) X, ...@@ -2421,7 +2421,7 @@ Lemma Group_add : forall a (x:a) A `{Inhab A} (M:map a A) (G:htype A a) X,
Heapdata G -> Heapdata G ->
Group G M \* (x ~> G X) ==> Group G (M[x:=X]). Group G M \* (x ~> G X) ==> Group G (M[x:=X]).
Proof using. Proof using.
intros. hchange~ Group_add_fresh. hsimpl. hsimpl. intros. hchange~ Group_add_fresh. hsimpl.
Qed. Qed.
(* LATER: prove reciprocal to Group_add (* LATER: prove reciprocal to Group_add
...@@ -2575,7 +2575,7 @@ Proof using. ...@@ -2575,7 +2575,7 @@ Proof using.
rewrite star_assoc. exists~ h1 h2. rewrite star_assoc. exists~ h1 h2.
auto. auto.
intros x. hchange (Qle' x). hchange~ (Qle x). intros x. hchange (Qle' x). hchange~ (Qle x).
set (H' := \GC) at 1 2. hsimpl; subst H'; affine. hchange (@hsimpl_gc (\GC \* \GC)). affine. hsimpl.
apply~ local_erase. apply~ local_erase.
Qed. Qed.
......
...@@ -108,8 +108,8 @@ Lemma iter_spec_rest : forall A (l:list A) (f:func), ...@@ -108,8 +108,8 @@ Lemma iter_spec_rest : forall A (l:list A) (f:func),
Proof using. Proof using.
=>> M. xapp~ (fun k => Hexists r, \[l = k ++ r] \* I r). =>> M. xapp~ (fun k => Hexists r, \[l = k ++ r] \* I r).
{ =>> E. xpull ;=> r' E'. subst l. { =>> E. xpull ;=> r' E'. subst l.
lets: app_cancel_l E'. subst r'. lets: app_cancel_l E'. subst r'.
xapp. xsimpl~. xsimpl~. } xapp. xsimpl~. }
{ xpull ;=>> E. rewrites (>> self_eq_app_l_inv E). xsimpl~. } { xpull ;=>> E. rewrites (>> self_eq_app_l_inv E). xsimpl~. }
Qed. (* TODO: beautify this proof *) Qed. (* TODO: beautify this proof *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment