From f116dde7daadaffc015e06b3c38a57398bfe0ef4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 12 Nov 2008 15:04:41 +0000 Subject: [PATCH] better names --- .../models/nat_dedekind_sigma_complete.ma | 46 +++++++++---------- 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma index b65653dfe..73211e023 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma @@ -30,12 +30,12 @@ alias symbol "N" = "ordered set N". lemma nat_dedekind_sigma_complete: ∀sg:‡ℕ.∀a:sequence {[sg]}. a is_increasing → - ∀x.x is_supremum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j). -intros 4; cases x (s Hs); clear x; letin X ≝ ≪s,Hs≫; + ∀X.X is_supremum a → ∃i.∀j.i ≤ j → \fst X = \fst (a j). +intros 4; cases X (x Hx); clear X; letin X ≝ ≪x,Hx≫; fold normalize X; intros; cases H1; alias symbol "N" = "Natural numbers". -letin spec ≝ (λi,j:ℕ.(𝕦_sg ≤ i ∧ s = \fst (a j)) ∨ (i < 𝕦_sg ∧ s + i ≤ 𝕦_sg + \fst (a j))); -(* s - aj <= max 0 (u - i) *) +letin spec ≝ (λi,j:ℕ.(𝕦_sg ≤ i ∧ x = \fst (a j)) ∨ (i < 𝕦_sg ∧ x + i ≤ 𝕦_sg + \fst (a j))); +(* x - aj <= max 0 (u - i) *) letin m ≝ (hide ? ( let rec aux i ≝ match i with @@ -43,29 +43,29 @@ letin m ≝ (hide ? ( | S m ⇒ let pred ≝ aux m in let apred ≝ a pred in - match cmp_nat s (\fst apred) with + match cmp_nat x (\fst apred) with [ cmp_le _ ⇒ pred | cmp_gt nP ⇒ \fst (H3 apred ?)]] in aux : ∀i:nat.∃j:nat.spec i j));[whd; apply nP;] unfold spec in aux ⊢ %; [3: unfold X in H2; clear H4 n aux spec H3 H1 H X; - cases (cases_in_segment ??? Hs); + cases (cases_in_segment ??? Hx); elim 𝕦_sg in H1 ⊢ %; intros (a Hs H); [1: left; split; [apply le_n] generalize in match H; - generalize in match Hs; - rewrite > (?:s = O); - [2: cases Hs; lapply (os_le_to_nat_le ?? H1); - apply (symmetric_eq nat O s ?).apply (le_n_O_to_eq s ?).apply (Hletin). + generalize in match Hx; + rewrite > (?:x = O); + [2: cases Hx; lapply (os_le_to_nat_le ?? H1); + apply (symmetric_eq nat O x ?).apply (le_n_O_to_eq x ?).apply (Hletin). |1: intros; unfold Type_of_ordered_set in sg; - lapply (H2 O) as K; lapply (sl2l ?? (a O) ≪s,Hs≫ K) as P; + lapply (H2 O) as K; lapply (sl2l ?? (a O) ≪x,Hx≫ K) as P; simplify in P:(???%); lapply (le_transitive ??? P H1) as W; lapply (os_le_to_nat_le ?? W) as R; apply (le_n_O_to_eq (\fst (a O)) R);] - |2: right; cases Hs; rewrite > (sym_plus s O); split; [apply le_S_S; apply le_O_n]; + |2: right; cases Hx; rewrite > (sym_plus x O); split; [apply le_S_S; apply le_O_n]; apply (trans_le ??? (os_le_to_nat_le ?? H3)); apply le_plus_n_r;] -|2: clear H6; cut (s = \fst (a (aux n1))); [2: +|2: clear H6; cut (x = \fst (a (aux n1))); [2: cases (le_to_or_lt_eq ?? H5); [2: assumption] cases (?:False); apply (H2 (aux n1) H6);] clear H5; generalize in match Hcut; clear Hcut; intro H5; @@ -80,21 +80,21 @@ letin m ≝ (hide ? ( [1,3: left; split; [1,3: assumption |2: assumption] cut (𝕦_sg = S n1); [2: apply le_to_le_to_eq; assumption ] clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut; - cut (s = S (\fst (a w))); + cut (x = S (\fst (a w))); [2: apply le_to_le_to_eq; [2: assumption] - change in H8 with (s + n1 ≤ S (n1 + \fst (a w))); + change in H8 with (x + n1 ≤ S (n1 + \fst (a w))); rewrite > plus_n_Sm in H8; rewrite > sym_plus in H8; apply (le_plus_to_le ??? H8);] cases (H3 (a w) H6); - change with (s = \fst (a w1)); + change with (x = \fst (a w1)); change in H4 with (\fst (a w) < \fst (a w1)); apply le_to_le_to_eq; [ rewrite > Hcut; assumption ] - apply (os_le_to_nat_le (\fst (a w1)) s (H2 w1)); + apply (os_le_to_nat_le (\fst (a w1)) x (H2 w1)); |*: right; split; try assumption; [1: rewrite > sym_plus in ⊢ (? ? %); rewrite < H6; apply le_plus_r; assumption; |2: cases (H3 (a w) H6); - change with (s + S n1 ≤ 𝕦_sg + \fst (a w1));rewrite < plus_n_Sm; + change with (x + S n1 ≤ 𝕦_sg + \fst (a w1));rewrite < plus_n_Sm; apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm; apply (le_plus ???? (le_n ?) H9);]]]] clearbody m; unfold spec in m; clear spec; @@ -102,25 +102,25 @@ letin find ≝ ( let rec find i u on u : nat ≝ match u with [ O ⇒ (m i:nat) - | S w ⇒ match eqb (\fst (a (m i))) s with + | S w ⇒ match eqb (\fst (a (m i))) x with [ true ⇒ (m i:nat) | false ⇒ find (S i) w]] in find : - ∀i,bound.∃j.i + bound = 𝕦_sg → s = \fst (a j)); -[1: cases (find (S n) n2); intro; change with (s = \fst (a w)); + ∀i,bound.∃j.i + bound = 𝕦_sg → x = \fst (a j)); +[1: cases (find (S n) n2); intro; change with (x = \fst (a w)); apply H6; rewrite < H7; simplify; apply plus_n_Sm; |2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity |3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1; cases (m 𝕦_sg); cases H4; clear H4; cases H5; clear H5; [assumption] cases (not_le_Sn_n ? H4)] clearbody find; cases (find O 𝕦_sg); -exists [apply w]; intros; change with (s = \fst (a j)); +exists [apply w]; intros; change with (x = \fst (a j)); rewrite > (H4 ?); [2: reflexivity] apply le_to_le_to_eq; [1: apply os_le_to_nat_le; apply (trans_increasing ? H ? ? (nat_le_to_os_le ?? H5)); -|2: apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);] +|2: apply (trans_le ? x ?);[apply os_le_to_nat_le; apply (H2 j);] rewrite < (H4 ?); [2: reflexivity] apply le_n;] qed. -- 2.39.2