From 488f469606b3e80aa395cb29273c932c0558815a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 25 Oct 2008 17:14:37 +0000
Subject: [PATCH] ...

---
 .../matita/contribs/didactic/duality.ma       | 43 ++++++++++++-------
 1 file changed, 27 insertions(+), 16 deletions(-)

diff --git a/helm/software/matita/contribs/didactic/duality.ma b/helm/software/matita/contribs/didactic/duality.ma
index 4f16daf04..fd8e0d17a 100644
--- a/helm/software/matita/contribs/didactic/duality.ma
+++ b/helm/software/matita/contribs/didactic/duality.ma
@@ -1,9 +1,11 @@
 
 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
@@ -72,28 +74,37 @@ let rec dualize (F : Formula) on F : Formula ≝
   | 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 :
-- 
2.39.2