Commit 976c58f3 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 b37d0fec
...@@ -390,7 +390,7 @@ Section simple_collection. ...@@ -390,7 +390,7 @@ Section simple_collection.
split. split.
- induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|]. - 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. 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. intros. apply elem_of_union_r; auto.
Qed. Qed.
......
...@@ -926,7 +926,7 @@ Proof. by destruct n. Qed. ...@@ -926,7 +926,7 @@ Proof. by destruct n. Qed.
Lemma drop_length l n : length (drop n l) = length l - n. Lemma drop_length l n : length (drop n l) = length l - n.
Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed. Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed.
Lemma drop_ge l n : length l n drop n l = []. 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 = []. Lemma drop_all l : drop (length l) l = [].
Proof. by apply drop_ge. Qed. Proof. by apply drop_ge. Qed.
Lemma drop_drop l n1 n2 : drop n1 (drop n2 l) = drop (n2 + n1) l. Lemma drop_drop l n1 n2 : drop n1 (drop n2 l) = drop (n2 + n1) l.
...@@ -2828,7 +2828,7 @@ Section fmap. ...@@ -2828,7 +2828,7 @@ Section fmap.
( x, f x = y) f <$> l = replicate (length l) y. ( x, f x = y) f <$> l = replicate (length l) y.
Proof. intros; induction l; f_equal/=; auto. Qed. Proof. intros; induction l; f_equal/=; auto. Qed.
Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i). 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 : Lemma list_lookup_fmap_inv l i x :
(f <$> l) !! i = Some x y, x = f y l !! i = Some y. (f <$> l) !! i = Some x y, x = f y l !! i = Some y.
Proof. 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