-set "baseuri" "cic:/matita/tests/".
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
-inductive nat : Set \def
- O : nat
- | S : nat \to nat.
-
-inductive le (n:nat) : nat \to Prop \def
- leO : le n n
- | leS : \forall m. le n m \to le n (S m).
+set "baseuri" "cic:/matita/tests/inversion_sum/".
+include "legacy/coq.ma".
+
+
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
+alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
+
+inductive sum (n:nat) : nat \to nat \to Set \def
+ k: \forall x,y. n = x + y \to sum n x y.
-alias symbol "eq" (instance 0) = "leibnitz's equality".
-theorem test_inversion: \forall n. le n O \to n=O.
- intros.
- cut O=O.
- (* goal 2: 0 = 0 *)
- goal 7. reflexivity.
- (* goal 1 *)
- generalize Hcut. (* non attaccata. Dovrebbe dare 0=0 -> n=0 *)
- apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
- intro. reflexivity.
- simplify. intros.
- discriminate H3.
-qed.
-(* Piu' semplice e non lascia l'ipotesi inutile Hcut *)
-alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
-theorem test_inversion2: \forall n. le n O \to n=O.
+
+theorem t: \forall x,y. \forall H: sum x y O.
+ match H with [ (k a b p) \Rightarrow a ] = x.
intros.
- generalize (refl_equal nat O).
- apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
- intro. reflexivity.
+ inversion H.
+
+ (*
+ cut (y = y \to O = O \to match H with [ (k a b p) \Rightarrow a] = x).
+ apply Hcut; reflexivity.
+ apply
+ (sum_ind ?
+ (\lambda a,b,K. y=a \to O=b \to
+ match K with [ (k a b p) \Rightarrow a ] = x)
+ ? ? ? H).
+ goal 16.*)
simplify. intros.
- discriminate H3.
+ generalize in match H1.
+ rewrite < H2; rewrite < H3.intro.
+ rewrite > H4.auto.
+qed.
+
+theorem t1: \forall x,y. sum x y O \to x = y.
+intros.
+
+(*
+cut y=y \to O=O \to x = y.
+apply Hcut.reflexivity. reflexivity.
+apply (sum_ind ? (\lambda a,b,K. y=a \to O=b \to x=a) ? ? ? s).*)
+
+(*apply (sum_ind ? (\lambda a,b,K. y = a \to O = b \to x = a) ? ? ? s).*)
+inversion s.
+intros.simplify.
+intros.
+rewrite > H. rewrite < H2. auto.
qed.