Merge pull request #26 from ablearthy/coq20

coq-community · Nov 14, 2024 · 9b2874b · 9b2874b
2 parents 4e23c93 + 3d4a336
commit 9b2874b
Show file tree

Hide file tree

Showing 9 changed files with 24 additions and 23 deletions.
diff --git a/src/beyond.v b/src/beyond.v
@@ -1,6 +1,6 @@
 From Equations Require Import Equations.
 From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype order ssrnat seq path.
+From mathcomp Require Import ssrnat eqtype order seq path.
 From favssr Require Import prelude bintree bst adt redblack.
 
 Set Implicit Arguments.
@@ -504,7 +504,7 @@ Lemma invc2_joinL l x r :
   invc l -> invc r -> (bh l <= bh r)%N ->
   invc2 (joinL l x r) && ((bh l != bh r) && (color r == Black) ==> invc (joinL l x r)).
 Proof.
-funelim (joinL l x r); simp joinL; rewrite {}Heq /=.
+funelim (joinL l x r); try rewrite Heqcall; simp joinL; rewrite {}Heq /=.
 - rewrite /invc2; rewrite {}e /= addn0 in i *.
   have/negbTE->: (Red != Black) by [].
   rewrite andbF /= andbT=> Hcl /and3P [/andP [Hlrb _] Hclr -> E]; rewrite andbT.
@@ -525,7 +525,7 @@ Lemma bh_joinL l x r :
   invh l -> invh r -> (bh l <= bh r)%N ->
   bh (joinL l x r) == bh r.
 Proof.
-funelim (joinL l x r); simp joinL; rewrite {}Heq /=.
+funelim (joinL l x r); try rewrite Heqcall; simp joinL; rewrite {}Heq /=.
 - move=>Hl; rewrite {}e /= !addn0 => /and3P [_ Hlr _] E.
   by apply: H.
 - move=>Hl; rewrite {}e /= in i *; case/and3P=>E1 Hlr _ _.
@@ -540,7 +540,7 @@ Lemma invh_joinL l x r :
   invh l -> invh r -> (bh l <= bh r)%N ->
   invh (joinL l x r).
 Proof.
-funelim (joinL l x r); simp joinL; rewrite {}Heq /=.
+funelim (joinL l x r); try rewrite Heqcall; simp joinL; rewrite {}Heq /=.
 - move=>Hl; rewrite {Heqcall r}e /= addn0 in i *.
   case/and3P=>/eqP<- Hlr -> E; rewrite andbT.
   by apply/andP; split; [apply: bh_joinL | apply: H].
@@ -555,7 +555,7 @@ Qed.
 Lemma joinL_inorder l a r :
   inorder_a (joinL l a r) = inorder_a l ++ a :: inorder_a r.
 Proof.
-funelim (joinL l a r); simp joinL; rewrite {}Heq //= e /=.
+funelim (joinL l a r); try rewrite Heqcall; simp joinL; rewrite {}Heq //= e /=.
 - by rewrite H -catA.
 by rewrite inorder_baliL H -catA.
 Qed.
@@ -599,7 +599,7 @@ Lemma bst_joinL l a r :
   (bh l <= bh r)%N ->
   bst_a (joinL l a r).
 Proof.
-funelim (joinL l a r); simp joinL; rewrite {}Heq /=; last by move=>->->->->.
+funelim (joinL l a r); try rewrite Heqcall; simp joinL; rewrite {}Heq /=; last by move=>->->->->.
 - rewrite {}e /= addn0 all_cat /= => Hal /and3P [Halr Hx _] Hbl /and4P [Halr' -> Hblr ->] E /=.
   rewrite andbT; apply/andP; split; last by apply: H.
   rewrite joinL_inorder all_cat /= Hx Halr' /= andbT.
@@ -618,7 +618,7 @@ Lemma invc2_joinR l x r :
   invc l -> invc r -> invh l -> invh r -> (bh r <= bh l)%N ->
   invc2 (joinR l x r) && ((bh l != bh r) && (color l == Black) ==> invc (joinR l x r)).
 Proof.
-funelim (joinR l x r); simp joinR; rewrite {}Heq /=.
+funelim (joinR l x r); try rewrite Heqcall; simp joinR; rewrite {}Heq /=.
 - rewrite /invc2; rewrite {}e /= in i *.
   have/negbTE->: (Red != Black) by [].
   rewrite andbF /= andbT => /and3P [/andP [_ Hrlb] -> Hcrl] Hcr /and3P [/eqP E1 Hhll Hhrl] Hhr E /=.
@@ -641,7 +641,7 @@ Lemma bh_joinR l x r :
   invh l -> invh r -> (bh r <= bh l)%N ->
   bh (joinR l x r) == bh l.
 Proof.
-funelim (joinR l x r); simp joinR; rewrite {}Heq /= ?addn0 //.
+funelim (joinR l x r); try rewrite Heqcall; simp joinR; rewrite {}Heq /= ?addn0 //.
 - by rewrite {}e /= addn0.
 rewrite {}e /= in i *; case/and3P=>/eqP E1 Hll Hrl Hr ?.
 move: i; rewrite {1}addn1 ltnS E1=>E.
@@ -653,7 +653,7 @@ Lemma invh_joinR l x r :
   invh l -> invh r -> (bh r <= bh l)%N ->
   invh (joinR l x r).
 Proof.
-funelim (joinR l x r); simp joinR; rewrite {}Heq /=.
+funelim (joinR l x r); try rewrite Heqcall; simp joinR; rewrite {}Heq /=.
 - rewrite {Heqcall l i}e /=; case/and3P=>/eqP E1 -> Hrl Hr E /=; rewrite E1 addn0 in E *.
   by rewrite eq_sym; apply/andP; split; [apply: bh_joinR | apply: H].
 - rewrite {Heqcall l}e /= in i *; case/and3P=>/eqP E1 Hll Hrl ? ?.
@@ -667,7 +667,7 @@ Qed.
 Lemma joinR_inorder l a r :
   inorder_a (joinR l a r) = inorder_a l ++ a :: inorder_a r.
 Proof.
-funelim (joinR l a r); simp joinR; rewrite {}Heq //= e /=.
+funelim (joinR l a r); try rewrite Heqcall; simp joinR; rewrite {}Heq //= e /=.
 - by rewrite H -catA.
 by rewrite inorder_baliR H -catA.
 Qed.
@@ -707,7 +707,7 @@ Lemma bst_joinR l a r :
   bst_a l -> bst_a r ->
   bst_a (joinR l a r).
 Proof.
-funelim (joinR l a r); simp joinR; rewrite {}Heq /=; last by move=>->->->->.
+funelim (joinR l a r); try rewrite Heqcall; simp joinR; rewrite {}Heq /=; last by move=>->->->->.
 - rewrite {}e /= all_cat /= => /and3P [_ Hx Harl] Har /and4P [-> Harl' -> Hbrl] Hbr /=.
   apply/andP; split; last by apply: H.
   rewrite joinR_inorder all_cat /= Hx Harl' /=.

diff --git a/src/binom_heap.v b/src/binom_heap.v
@@ -1,5 +1,5 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype order ssrnat seq path bigop prime binomial.
+From mathcomp Require Import ssrnat eqtype order seq path bigop prime binomial.
 From favssr Require Import prelude basics priority.
 
 Set Implicit Arguments.

diff --git a/src/braun.v b/src/braun.v
@@ -1061,7 +1061,7 @@ Definition list_fast {T} (t : tree T) : seq T :=
 Lemma list_fast_rec_all_leaf {T} (ts : seq (tree T)) :
   all (fun t => ~~ is_node t) ts -> list_fast_rec ts = [::].
 Proof.
-funelim (list_fast_rec ts); rewrite -Heqcall //= => Ha.
+funelim (list_fast_rec ts); try rewrite -Heqcall; move=> //= Ha.
 move: {H H0}Hv; suff: omap value xs = [::] by move=>->.
 by apply/omap_empty/sub_all/Ha; case.
 Qed.

diff --git a/src/braun_queue.v b/src/braun_queue.v
@@ -1,6 +1,6 @@
 From Equations Require Import Equations.
 From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype order ssrnat seq.
+From mathcomp Require Import ssrnat eqtype order seq.
 From favssr Require Import prelude bintree braun priority.
 
 Set Implicit Arguments.
@@ -185,7 +185,7 @@ Lemma braun_sift_down (l : tree T) a r :
   braun l -> braun r ->
   braun (sift_down l a r).
 Proof.
-funelim (sift_down l a r); simp sift_down=>/=.
+funelim (sift_down l a r)=> //=; simp sift_down=>/=.
 - by move=>_ _ _; case: ifP.
 rewrite !eqn_add2r=>E; case/and3P=>E1 Hl1 Hr1; case/and3P=>E2 Hl2 Hr2.
 case: ifP=>/=.
@@ -222,7 +222,7 @@ Lemma heap_sift_down (l : tree T) a r :
   heap l -> heap r ->
   heap (sift_down l a r).
 Proof.
-funelim (sift_down l a r); simp sift_down=>/=.
+funelim (sift_down l a r)=> //=; simp sift_down=>/=.
 - case/orP; first by rewrite addn1.
   rewrite eqn_add2r addn_eq0; case/andP=>/eqP/size0leaf->/eqP/size0leaf->/= _ _ _ _.
   by case: ifP=>/=; rewrite !andbT // =>/negbT; rewrite -ltNge=>/ltW.

diff --git a/src/huffman.v b/src/huffman.v
@@ -1479,10 +1479,11 @@ move=>H10; case: leqP; rewrite !sortedByWeight_cons2.
 move=>H20; rewrite Hw /=.
 have Hm: maxn (height t2) (heightF l) = 0.
 - by apply/eqP; rewrite maxn_eq0 Hl andbT; apply/eqP.
-move: (H _ _ Ht erefl Hs Hm)=>/=.
+(move: (H _ _ Ht erefl Hs Hm)=>/=) || (move: (H t (t2 :: l) Ht erefl erefl Hs Hm)=>/=).
 by rewrite !height_0_cachedWeight // leqNgt H20 /=.
 Qed.
 
+
 (* minima *)
 
 Definition minima (t : tree A) (a b : A) : bool :=

diff --git a/src/leftist.v b/src/leftist.v
@@ -1,5 +1,5 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype order ssrnat seq path prime.
+From mathcomp Require Import ssrnat eqtype order seq path prime.
 From favssr Require Import prelude bintree priority.
 
 Set Implicit Arguments.

diff --git a/src/redblack.v b/src/redblack.v
@@ -188,7 +188,7 @@ Lemma invc_baliL l a r :
   invc2 l -> invc r -> invc (baliL l a r).
 Proof.
 rewrite /invc2.
-funelim (baliL l a r); simp baliL=>/= /[swap] ->; rewrite !andbT //.
+funelim (baliL l a r)=> //=; simp baliL=>/= /[swap] ->; rewrite !andbT //.
 - by case/and3P=>_->->.
 - by case/andP; case/and3P=>_->->->.
 by case/and4P; case/andP=>->->_->->.
@@ -761,7 +761,7 @@ Lemma invc_join l r :
   invc2 (join l r) &&
       ((color l == Black) && (color r == Black) ==> invc (join l r)).
 Proof.
-funelim (join l r); simp join=>/=.
+funelim (join l r); try clear Heqcall; simp join=>/=.
 - by move=>_ /[dup] /invc2I ->->/=; apply: implybT.
 - case: p=>a c; rewrite /invc2 /= =>/and3P [->->->] _; apply: implybT.
 - rewrite -!andbA andbT.
@@ -811,7 +811,7 @@ Lemma invh_join l r :
   invh l -> invh r -> bh l == bh r ->
   invh (join l r) && (bh (join l r) == bh l).
 Proof.
-funelim (join l r); simp join=>/=.
+funelim (join l r); try clear Heqcall; simp join=>/=.
 - by move=>_->; rewrite eq_sym.
 - by case: p=>_ c->; rewrite eq_refl.
 - case/and3P=>/eqP E12 H1 H2; case/and3P=>/eqP E34 H3 H4.

diff --git a/src/selection.v b/src/selection.v
@@ -323,7 +323,7 @@ Qed.
 Lemma chop_size n xs :
   0 < n -> size (chop n xs) = up_div (size xs) n.
 Proof.
-funelim (chop n xs)=>// /H /= {H}IH.
+funelim(chop n xs); try rewrite Heqcall; move=> // /H /= {H}IH.
 case/boolP: (n <= size l)%N; last first.
 - rewrite -ltnNge=>Hk; move: (ltn_trans Hk (ltnSn n))=>{}Hk.
   by rewrite chop_ge_length_eq //= up_divS divn_small.

diff --git a/src/twothree.v b/src/twothree.v
@@ -1,6 +1,6 @@
 From Equations Require Import Equations.
 From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype order ssrnat seq path.
+From mathcomp Require Import ssrnat eqtype order seq path.
 From favssr Require Import prelude bst adt.
 
 Set Implicit Arguments.