Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • mayero/coq-num-analysis
  • hamelin/test-ci-coq-num-analysis
  • arias/coq-num-analysis
3 results
Show changes
Commits on Source (2)
...@@ -302,6 +302,11 @@ Lemma nat_sub2_r : ...@@ -302,6 +302,11 @@ Lemma nat_sub2_r :
forall m n, (n <= m)%coq_nat -> (m - (m - n)%coq_nat)%coq_nat = n. forall m n, (n <= m)%coq_nat -> (m - (m - n)%coq_nat)%coq_nat = n.
Proof. lia. Qed. Proof. lia. Qed.
Lemma nat_sub_r_monot :
forall m n p, (m <= p)%coq_nat -> (n <= p)%coq_nat ->
(m < n)%coq_nat -> ((p - n)%coq_nat < (p - m)%coq_nat)%coq_nat.
Proof. lia. Qed.
Lemma nat_double_S : forall n, (2 * n.+1)%coq_nat = (2 * n)%coq_nat.+2. Lemma nat_double_S : forall n, (2 * n.+1)%coq_nat = (2 * n)%coq_nat.+2.
Proof. intros; rewrite Nat.mul_succ_r; apply nat_add_2_r. Qed. Proof. intros; rewrite Nat.mul_succ_r; apply nat_add_2_r. Qed.
......
...@@ -4413,10 +4413,13 @@ Lemma insertF_revF : ...@@ -4413,10 +4413,13 @@ Lemma insertF_revF :
forall {n} i0 x0 (A : 'E^n), forall {n} i0 x0 (A : 'E^n),
insertF i0 x0 (revF A) = revF (insertF (rev_ord i0) x0 A). insertF i0 x0 (revF A) = revF (insertF (rev_ord i0) x0 A).
Proof. Proof.
intros; rewrite (insertF_permutF rev_ord_inj). unfold revF. intros n i0 x0 A; rewrite (insertF_permutF rev_ord_inj); unfold revF.
extF i; rewrite !permutF_correct; destruct (ord_eq_dec i i0) as [-> | Hi].
rewrite insert_f_ord_correct_l// !insertF_correct_l//.
Admitted. move: (skip_ord_correct_m i0) (inj_contra rev_ord_inj _ _ Hi) => H1 H2.
rewrite insert_f_ord_correct_r !insertF_correct_r
insert_skip_ord rev_insert_ord; easy.
Qed.
Lemma revF_insertF : Lemma revF_insertF :
forall {n} i0 x0 (A : 'E^n), forall {n} i0 x0 (A : 'E^n),
......
...@@ -2431,6 +2431,26 @@ Proof. intros; apply injF_surj, rev_ord_inj. Qed. ...@@ -2431,6 +2431,26 @@ Proof. intros; apply injF_surj, rev_ord_inj. Qed.
Lemma rev_ord_max : forall {n}, rev_ord (@ord_max n) = ord0. Lemma rev_ord_max : forall {n}, rev_ord (@ord_max n) = ord0.
Proof. intros; apply ord_inj; simpl; apply subnn. Qed. Proof. intros; apply ord_inj; simpl; apply subnn. Qed.
Lemma rev_ord_monot :
forall {n} {i j : 'I_n}, (i < j)%coq_nat -> (rev_ord j < rev_ord i)%coq_nat.
Proof.
move=>> H; rewrite !rev_ord_correct -minusE; apply nat_sub_r_monot;
[apply /leP.. | rewrite -Nat.succ_lt_mono]; easy.
Qed.
Lemma rev_insert_ord :
forall {n} {i0 i : 'I_n.+1} (H1 : i <> i0) (H2 : rev_ord i <> rev_ord i0),
rev_ord (insert_ord H1) = insert_ord H2.
Proof.
intros n i0 i H1 H2; destruct (lt_eq_lt_dec i i0) as [[H3 | H3] | H3];
[| contradict H1; apply ord_inj; easy |];
move: (rev_ord_monot H3) => H4.
rewrite insert_ord_correct_l insert_ord_correct_r; apply ord_inj; simpl.
rewrite -minusE; lia.
rewrite insert_ord_correct_r insert_ord_correct_l; apply ord_inj; simpl.
rewrite -minusE; lia.
Qed.
Lemma cast_f_rev_ord : Lemma cast_f_rev_ord :
forall {n1 n2} (H : n1 = n2), cast_f_ord H (@rev_ord n1) = @rev_ord n2. forall {n1 n2} (H : n1 = n2), cast_f_ord H (@rev_ord n1) = @rev_ord n2.
Proof. intros; subst; fun_ext; apply ord_inj; easy. Qed. Proof. intros; subst; fun_ext; apply ord_inj; easy. Qed.
......