fix

diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma
index fb0c1b0c4b473573d6853d2a44f2ddb7a7a81c40..f9b8a0fb6cc73bf8d848b2fdf2c366e8835ac8c0 100644 (file)
--- a/helm/matita/tests/match.ma
+++ b/helm/matita/tests/match.ma
@@ -177,6 +177,36 @@ intro.cut \forall m:nat.R n m.apply Hcut.elim n.apply H.
 apply nat_case m1.apply H1.intro.apply H2. apply H3.
 qed.
 
+inductive bool : Set \def 
+  | true : bool
+  | false : bool.
+
+definition notn : bool \to bool \def
+\lambda b:bool. 
+ match b with 
+ [ true \Rightarrow false
+ | false \Rightarrow true ].
+
+definition andb : bool \to bool \to bool\def
+\lambda b1,b2:bool. 
+ match b1 with 
+ [ true \Rightarrow 
+       match b2 with [true \Rightarrow true | false \Rightarrow false]
+ | false \Rightarrow false ].
+
+definition orb : bool \to bool \to bool\def
+\lambda b1,b2:bool. 
+ match b1 with 
+ [ true \Rightarrow 
+       match b2 with [true \Rightarrow true | false \Rightarrow false]
+ | false \Rightarrow false ].
+
+definition if_then_else : bool \to Prop \to Prop \to Prop \def 
+\lambda b:bool.\lambda P,Q:Prop.
+match b with
+[ true \Rightarrow P
+| false  \Rightarrow Q].
+
 inductive le (n:nat) : nat \to Prop \def
   | le_n : le n n
   | le_S : \forall m:nat. le n m \to le n (S m).
@@ -188,7 +218,7 @@ apply le_S.assumption.
 qed.
 
 theorem le_n_S: \forall n,m:nat. le n m \to le (S n) (S m).
-intro.elim H.alias id "le_n" = "cic:/matita/andrea/le.ind#xpointer(1/1/1)".
+intro.elim H.
 apply le_n.apply le_S.assumption.
 qed.
 
@@ -232,7 +262,7 @@ qed.
 theorem le_antisym : \forall n,m:nat. (le n m) \to (le m n) \to (eq nat n m).
 intro.cut (le n m) \to (le m n) \to (eq nat n m).exact Hcut H H1.
 apply nat_double_ind (\lambda n,m.((le n m) \to (le m n) \to eq nat n m)).
-intro.whd.intro.alias id "le_n_O_eq" = "cic:/matita/andrea/le_n_O_eq.con".
+intro.whd.intro.
 apply le_n_O_eq.assumption.
 intro.whd.intro.apply sym_eq.apply le_n_O_eq.assumption.
 intro.whd.intro.apply f_equal.apply H2.
@@ -240,30 +270,6 @@ apply le_S_n.assumption.
 apply le_S_n.assumption.
 qed.
 
-inductive bool : Set \def 
-  | true : bool
-  | false : bool.
-
-definition notn : bool \to bool \def
-\lambda b:bool. 
- match b with 
- [ true \Rightarrow false
- | false \Rightarrow true ].
-
-definition andb : bool \to bool \to bool\def
-\lambda b1,b2:bool. 
- match b1 with 
- [ true \Rightarrow 
-       match b2 with [true \Rightarrow true | false \Rightarrow false]
- | false \Rightarrow false ].
-
-definition orb : bool \to bool \to bool\def
-\lambda b1,b2:bool. 
- match b1 with 
- [ true \Rightarrow 
-       match b2 with [true \Rightarrow true | false \Rightarrow false]
- | false \Rightarrow false ].
-
 definition leb : nat \to nat \to bool \def
 let rec leb (n,m:nat) \def 
    [\lambda n:nat.bool] match n:nat with 
@@ -274,98 +280,13 @@ let rec leb (n,m:nat) \def
        | (S q) \Rightarrow leb p q]]
 in leb.
 
-definition if_then_else : bool \to Prop \to Prop \to Prop \def 
-\lambda b:bool.\lambda P,Q:Prop.
-match b with
-[ true \Rightarrow P
-| false  \Rightarrow Q].
-
 theorem le_dec: \forall n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m)).
-intro.
+intros.
 apply (nat_double_ind 
-(\lambda n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m))) ? ? ? n m).
-intro.whd.apply le_O_n.intro.whd.apply le_Sn_O.
-
-intros 2.
-simplify.
-cut ((
-
-\lambda b:bool. [\lambda x:bool.Prop] match b:bool with 
-[ true \Rightarrow (le n1 m1) 
-| false \Rightarrow (Not(le n1 m1))]
-
-\to
-
- [\lambda x:bool.Prop] match b:bool with 
-[ true \Rightarrow (le (S n1) (S m1)) 
-| false \Rightarrow (Not(le (S n1) (S m1)))]
-) (leb n1 m1)).
-goal 8.
-
-exact (
-[
-\lambda b:bool. [\lambda x:bool.Prop] match b:bool with 
-[ true \Rightarrow (le n1 m1) 
-| false \Rightarrow (Not(le n1 m1))]
-
-\to
-
- [\lambda x:bool.Prop] match b:bool with 
-[ true \Rightarrow (le (S n1) (S m1)) 
-| false \Rightarrow (Not(le (S n1) (S m1)))]
-
-]
-match (leb n1 m1) : bool with 
-[ true \Rightarrow \lambda p:(le n1 m1). le_n_S n1 m1 p
-| false \Rightarrow \lambda p:(Not(le n1 m1)). \lambda q:(le (S n1) (S m1)).p(le_S_n n1 m1 q)]
-).
-apply Hcut.
-
-
-cut (eq bool (leb n1 m1) (leb (S n1) (S m1))).
-goal 8.
-simplify.apply refl_equal.
-cut 
-  (if_then_else 
-     (leb (S n1) (S m1)) 
-     (le (S n1) (S m1)) 
-     (Not (le (S n1) ( S m1)) )).
-apply Hcut1.elim Hcut.simplify.
-check ([\lambda b:bool. [\lambda b:bool.Prop]match (b:bool) with 
-     [ true \Rightarrow 
-             (if_then_else b (le n1 m1) (Not (le  n1 m1)))
-     | false \Rightarrow 
-             (if_then_else b (le n1 m1) (Not (le  n1 m1)))
-]
-]
-match (leb n1 m1) : bool with 
-[ true \Rightarrow H | false \Rightarrow H ]).
-
-
-exact (
-[\lambda b:bool. match (b:bool) with 
-     [ true \Rightarrow 
-             (if_then_else b (le (S n1 ) (S m1)) (Not ((le (S n1) (S m1)))))
-     | false \Rightarrow 
-             (if_then_else b (le (S n1 ) (S m1)) (Not ((le (S n1) (S m1)))))
-]
-]
-match (leb n1 m1) : bool with 
-[ true \Rightarrow le_n_S n1 m1 H
-| false \Rightarrow  
-      (\lambda p:(le (S n1) (S m1)).H (le_S_n n1 m1 p))]).
-
-
-
-
-elim n.simplify.apply le_O_n.elim m.
-simplify.apply le_Sn_O.simplify.
-cut (match (leb e e1):bool with 
-[true \Rightarrow (eq bool (leb e e1) true)
-| false \Rightarrow (eq bool (leb e e1) false)]).
-goal 20.
-exact [\lambda b:bool. match b with 
-[true \Rightarrow (eq bool b true)
-| false \Rightarrow (eq bool b false)]] match (leb e e1):bool with 
-[true \Rightarrow refl_equal bool true
-| false \Rightarrow refl_equal bool false].
\ No newline at end of file
+(\lambda n,m:nat.if_then_else (leb n m) (le n m) (Not (le n m))) ? ? ? n m).
+simplify.intros.apply le_O_n.
+simplify.exact le_Sn_O.
+intros 2.simplify.elim (leb n1 m1).
+simplify.apply le_n_S.apply H.
+simplify.intro.apply H.apply le_S_n.assumption.
+qed.