Commit ae135201 authored by Ralf Jung's avatar Ralf Jung

Better Coq 8.6 compatibility

With Coq 8.6, you can no longer have intro patterns that give more names than
the constructor has.  Also, patterns with too few names are now interpreted as
filling up with "?", rather than putting the unnamed parts into the goal again.

Furthermore, it seems the behavior of "simplify_eq/=" changed, I guess
hypotheses are considered in different order now.  I managed to work around
this, but it all seem kind of fragile.

The next compilation failure is an "Anyomaly: ... Please report", so that's what I will do.
parent b5e8ab4e
......@@ -109,14 +109,14 @@ Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) :
gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
Proof.
assert (i = i2 + i1) by lia; simplify_eq/=. revert j x H1.
assert (i = i2 + i1) by lia; move:H1=>H1; simplify_eq/=. revert j x H1.
induction i2 as [|i2 IH]; intros j X H1; simplify_eq/=;
[by rewrite coerce_id|by rewrite g_coerce IH].
Qed.
Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) :
coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)).
Proof.
assert (i = i1 + i2) by lia; simplify_eq/=.
assert (i = i1 + i2) by lia; move:H1=>H1; simplify_eq/=.
induction i1 as [|i1 IH]; simplify_eq/=;
[by rewrite coerce_id|by rewrite coerce_f IH].
Qed.
......
......@@ -390,7 +390,7 @@ Section simple_collection.
split.
- induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|].
setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver.
- intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
- intros [X [Hx]]. induction Hx; simpl; [by apply elem_of_union_l |].
intros. apply elem_of_union_r; auto.
Qed.
......
......@@ -926,7 +926,7 @@ Proof. by destruct n. Qed.
Lemma drop_length l n : length (drop n l) = length l - n.
Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed.
Lemma drop_ge l n : length l n drop n l = [].
Proof. revert n. induction l; intros [|??]; simpl in *; auto with lia. Qed.
Proof. revert n. induction l; intros [|?]; simpl in *; auto with lia. Qed.
Lemma drop_all l : drop (length l) l = [].
Proof. by apply drop_ge. Qed.
Lemma drop_drop l n1 n2 : drop n1 (drop n2 l) = drop (n2 + n1) l.
......@@ -2828,7 +2828,7 @@ Section fmap.
( x, f x = y) f <$> l = replicate (length l) y.
Proof. intros; induction l; f_equal/=; auto. Qed.
Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
Proof. revert i. induction l; by intros [|]. Qed.
Proof. revert i. induction l; intros [|n]; by try revert n. Qed.
Lemma list_lookup_fmap_inv l i x :
(f <$> l) !! i = Some x y, x = f y l !! i = Some y.
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