...

diff --git a/helm/software/matita/contribs/didactic/duality.ma b/helm/software/matita/contribs/didactic/duality.ma
index 4f16daf04492267f42bc18571859215e7de8fe08..fd8e0d17a2f7c6b9acc0d05ba798e8092811546c 100644 (file)
--- a/helm/software/matita/contribs/didactic/duality.ma
+++ b/helm/software/matita/contribs/didactic/duality.ma
@@ -1,9 +1,11 @@
 
 include "nat/minus.ma".
 
 include "nat/minus.ma".

-definition max : nat → nat → nat ≝ λa,b:nat.let rec max n m on n ≝ match n with [ O ⇒ b | S n ⇒ match m with [ O ⇒ a | S m ⇒ max n m]] in max a b.
-definition min : nat → nat → nat ≝ λa,b:nat.let rec min n m on n ≝ match n with [ O ⇒ a | S n ⇒ match m with [ O ⇒ b | S m ⇒ min n m]] in min a b.
-
-
+let rec max n m on n ≝ 
+    match n with [ O ⇒ m | S n ⇒ 
+    match m with [ O ⇒ S n | S m ⇒ S (max n m)]].
+let rec min n m on n ≝ 
+    match n with [ O ⇒ O | S n ⇒ 
+    match m with [ O ⇒ O | S m ⇒ S (min n m)]].

 
 inductive Formula : Type ≝
 | FBot: Formula
 
 inductive Formula : Type ≝
 | FBot: Formula


@@ -72,28 +74,37 @@ let rec dualize (F : Formula) on F : Formula ≝
   | FNot F ⇒ FNot (dualize F)
   ].
 
   | FNot F ⇒ FNot (dualize F)
   ].
 

+lemma max_n_O : ∀n. max n O = n. intros; cases n; reflexivity; qed.

 
 

-lemma : F[G/x] ≡ F
-
-
-
-
-
-
-
+lemma min_n_n : ∀n. min n n = n. intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity; qed.

 
 

+lemma min_le: ∀m,n. n ≤ m → min n m = n.
+intro; elim m; [cases n in H; intros; [reflexivity] cases (not_le_Sn_O ? H)]
+cases n1 in H1; 

 
 
 
 

+lemma xxx : ∀a,b,c.min (min a b) c = min a (min b c).
+intros; elim a; [reflexivity] elim b in c H 0; [intros;reflexivity] intros;
+lapply depth=0 (H O);

 
 
 
 

+simplify in ⊢ (? ? ? (? ? %));
+simplify in ⊢ (? ? (? % ?) ?);
+simplify in H:(? ? (? % ?) ?);
+simplify in H:(? ? ? (? ? %));
+simplify in ⊢ (? ? ? %);reflexivity]
+simplify in ⊢ (? ? (? % ?) ?);reflexivity]
+*)
+lemma min_minus_n_m : ∀n,m. min (n-m) n = n-m.
+intros; apply (nat_elim2 ???? n m); intros; [reflexivity]
+[ rewrite < minus_n_O; apply min_n_n]

 
 
 
 

-lemma max_n_O : ∀n. max n O = n. intros; cases n; reflexivity; qed.
+ cases m; [ rewrite < minus_n_O; apply min_n_n]

 
 

-lemma min_n_n : ∀n. min n n = n. intros; elim n; [reflexivity] simplify;assumption;
+lapply (H (S w)) as K; rewrite < minus_n_O in K; apply eq_f; assumption;] 
+rewrite < (H n2) in ⊢ (? ? ? %);

 
 

-lemma min_minus_n_m : ∀n,m. min (n-m) n = n-m. intro; elim n; try reflexivity;
-cases m; [

 simplify in ⊢ (? ? (? % ?) ?);simplify; rewrite > (H n1);
 
 lemma min_one :
 simplify in ⊢ (? ? (? % ?) ?);simplify; rewrite > (H n1);
 
 lemma min_one :