From f3ef6e0ddbdbbba26ea84b49609aadb7bd58348f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Wed, 7 Feb 2024 17:23:44 +0100
Subject: [PATCH] Rm temporary annotations.
---
FEM/Algebra/Finite_family.v | 6 ------
FEM/Algebra/ord_compl.v | 16 ----------------
2 files changed, 22 deletions(-)
diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index dc741fdd..2bfd993d 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -1538,7 +1538,6 @@ rewrite -Hp'2; unfold f'; rewrite widen_narrow_S.
contradict Hi1; apply Hf; easy.
Qed.
-(* A MONTRER B0 *)
Lemma injF_restr_bij_EX :
forall {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f),
{ p1 : 'I_[n1] | bijective p1 /\ incrF (f \o p1) }.
@@ -4884,7 +4883,6 @@ contradict Hi2; rewrite not_all_not_ex_equiv.
destruct (HP i2) as [[i1 Hi1] | Hi2]; [exists i1 |]; easy.
Qed.
-(* A MONTRER A2b *)
Lemma filterP_ord_Rg :
forall {n1 n2} {f : 'I_{n1,n2}} (Hf : incrF f)
{P1 : 'Prop^n1} {P2 : 'Prop^n2} (HP : extendPF f P1 P2),
@@ -4926,7 +4924,6 @@ apply Nat.lt_le_incl, Hf; simpl.
apply Nat.neq_0_lt_0, (ord_neq_compat Ht).
Qed.
-(* A MONTRER A2a *)
Lemma fun_ext_incrF_Rg :
forall {n1 n2} {f g : 'I_{n1,n2}},
incrF f -> incrF g -> Rg f = Rg g -> f = g.
@@ -4944,7 +4941,6 @@ move=> i2 -> H1; inversion H1 as [i1 _ Hi1]; apply (incrF_inj Hg) in Hi1; easy.
apply trans_eq with (Rg f); [apply sym_eq | rewrite HRg H0]; apply Rg_0_liftF_S.
Qed.
-(* A MONTRER A1b *)
Lemma filterP_ord_w_incrF :
forall {n1 n2} {f : 'I_{n1,n2}} (Hf : incrF f) {P1 : 'Prop^n1}
{P2 : 'Prop^n2} (HP : extendPF f P1 P2),
@@ -4957,7 +4953,6 @@ apply filterP_cast_ord_incrF.
apply filterP_ord_Rg.
Qed.
-(* A MONTRER A1a *)
Lemma filterP_f_ord_w_incrF :
forall {n1 n2} {f : 'I_{n1,n2}} (Hf : incrF f)
{P1 : 'Prop^n1} {P2 : 'Prop^n2} (HP : extendPF f P1 P2)
@@ -5027,7 +5022,6 @@ rewrite HA2; [ apply maskPF_correct_r; rewrite -Rg_compl_equiv |];
rewrite Rg_compl; easy.
Qed.
-(* A MONTRER A0 *)
Lemma filterPF_unfunF :
forall {F : Type} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
{P1 : 'I_n1 -> Prop} {P2 : 'I_n2 -> Prop} (HP : extendPF f P1 P2)
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index c55c3f27..5e544512 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -122,7 +122,6 @@ Section Seq_compl3.
Context {T : eqType}.
-(* A MONTRER B3b *)
Lemma injS_equiv_seq :
forall {P : pred T} {sT : subType P} {f : T -> sT},
injS P f <-> forall s, all P s -> { in s &, injective f }.
@@ -660,7 +659,6 @@ Qed.
Lemma nth_ord_enum : forall {n} i0 {i : 'I_n}, nth i0 (ord_enum n) i = i.
Proof. intros n i0 [j Hj]; apply nth_ord_enum_alt. Qed.
-(* A MONTRER B2b *)
Lemma map_nth_ord_enum :
forall (l : seq T),
map (fun i : 'I_(size l) => nth x0 l i) (ord_enum (size l)) = l.
@@ -669,7 +667,6 @@ intros l; move: (map_nth_iota0 x0 (leqnn (size l))).
rewrite take_size -val_ord_enum -map_comp; easy.
Qed.
-(* A MONTRER B2c *)
Lemma map_nth_invF :
forall {n l1 l2}, size l1 = n.+1 -> size l2 = n.+1 ->
forall {p : 'I_[n.+1]} (Hp : injective p),
@@ -720,7 +717,6 @@ move=>> Hj1 Hj2; rewrite !in_ordS_correct_l_alt.
move=> /(f_equal (@nat_of_ord _)); easy.
Qed.
-(* A MONTRER B3a *)
Lemma ord_enumS_eq : forall {n}, ord_enum n.+1 = map in_ordS (iota 0 n.+1).
Proof.
intros n; apply (@eq_from_nth _ ord0).
@@ -742,7 +738,6 @@ Context {T : Type}.
Variable leT : rel T.
Variable x0 : T.
-(* A MONTRER B2a *)
Lemma perm_ord_enum_sort :
forall l,
{ il | perm_eq il (ord_enum (size l)) /\ uniq il &
@@ -777,7 +772,6 @@ Section Ord_compl3b.
Context {T : eqType}.
Context {leT : rel T}.
-(* A MONTRER A4c *)
Lemma sorted_ordP :
forall {l : seq T} x0 x1,
reflect (forall (i : 'I_(size l)) (Hi1 : i.+1 < size l),
@@ -797,7 +791,6 @@ Hypothesis HT2 : total leT.
Variable x0 : T.
-(* A MONTRER B1b *)
Lemma perm_EX :
forall {l1 l2}, perm_eq l1 l2 ->
{ p : 'I_[size l2] | injective p &
@@ -852,7 +845,6 @@ rewrite !(nth_map ord0)//; [| rewrite size_ord_enum; easy].
rewrite !nth_ord_enum; unfold q2; rewrite f_inv_correct_l; easy.
Qed.
-(* A MONTRER B1a *)
Lemma sort_perm_EX :
forall l, { p : 'I_[size l] | injective p &
sort leT l = map (fun i => nth x0 l (p i)) (ord_enum (size l)) }.
@@ -1042,7 +1034,6 @@ assert (Hj : (i + (j - i - 1) + 1 < n)) by now rewrite H3.
replace j with (Ordinal Hj); [apply HA | apply ord_inj; easy].
Qed.
-(* A MONTRER A3c *)
(* leT is assumed transitive. *)
Lemma sortedF_S_sortedF :
forall {n} {A : 'I_n -> T},
@@ -1068,7 +1059,6 @@ assert (H4 : (i + p + 1).+1 < n) by now rewrite H3.
replace (Ordinal H1) with (Ordinal H4); [apply HA | apply ord_inj; easy].
Qed.
-(* A MONTRER A3b *)
(* leT is assumed transitive. *)
Lemma sortedF_equiv :
forall {n} {A : 'I_n -> T},
@@ -1148,7 +1138,6 @@ Lemma ord_ltn_total_strict :
forall {n} (i j : 'I_n), i != j = ord_ltn i j || ord_ltn j i.
Proof. move=>>; apply neq_ltn. Qed.
-(* A MONTRER A4b *)
Lemma sorted_enum_ord : forall {n}, sorted ord_ltn (enum 'I_n).
Proof.
intros n; destruct n as [|n]; [rewrite (size0nil (size_enum_ord _)); easy |].
@@ -1156,7 +1145,6 @@ apply /(sortedP ord0); intros i Hi1; rewrite size_enum_ord in Hi1.
unfold ord_ltn; rewrite !nth_enum_ord//; apply ltn_trans with i.+1; easy.
Qed.
-(* A MONTRER A4a *)
Lemma sorted_filter_enum_ord :
forall {n} (P : 'I_n -> Prop),
sorted ord_ltn (filter (fun i => asbool (P i)) (enum 'I_n)).
@@ -1184,7 +1172,6 @@ Lemma incrF_inj :
forall {n1 n2} {f : 'I_{n1,n2}}, incrF f -> injective f.
Proof. move=>>; apply sortedF_inj, ord_lt_irrefl. Qed.
-(* A MONTRER A3a *)
Lemma incrF_equiv : forall {n1 n2} (f : 'I_{n1,n2}), incrF f <-> incrF_S f.
Proof. intros; apply sortedF_equiv, ord_lt_trans. Qed.
@@ -2472,7 +2459,6 @@ Lemma unfilterP_ord_inj :
unfilterP_ord HP0 i = unfilterP_ord HP0 j -> i = j.
Proof. move=>> Hi Hj; apply enum_rank_in_inj; apply /asboolP; easy. Qed.
-(* A MONTRER A2e *)
Lemma filterP_ord_incrF_S :
forall {n} (P : 'I_n -> Prop),
incrF_S (fun j : 'I_(lenPF P) => filterP_ord j).
@@ -2490,12 +2476,10 @@ assert (Hjj1 : jj.+1 < size (filter (fun i => asbool (P i)) (enum 'I_n)))
apply (H0 (enum_default j) (enum_default (Ordinal Hj1)) jj Hjj1).
Qed.
-(* A MONTRER A2d *)
Lemma filterP_ord_incrF :
forall {n} (P : 'I_n -> Prop), incrF (fun j : 'I_(lenPF P) => filterP_ord j).
Proof. intros; apply incrF_equiv, filterP_ord_incrF_S. Qed.
-(* A MONTRER A2c *)
Lemma filterP_cast_ord_incrF :
forall {n1 n2} {P1 : 'I_n1 -> Prop} {P2 : 'I_n2 -> Prop}
(H : lenPF P1 = lenPF P2),
--
GitLab