]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/tests/inversion.ma
update in basic_2
[helm.git] / matitaB / matita / tests / inversion.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15
16 include "coq.ma".
17
18
19 alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
20 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
21
22 inductive sum (n:nat) : nat \to nat \to Set \def
23   k: \forall x,y. n = x + y \to sum n x y.
24
25
26
27   
28 theorem t: \forall x,y. \forall H: sum x y O.
29           match H with [ (k a b p) \Rightarrow a ] = x.
30  intros.
31  inversion H.
32  
33  (*
34  cut (y = y \to O = O \to match H with [ (k a b p) \Rightarrow a] = x).
35  apply Hcut; reflexivity.
36  apply
37   (sum_ind ?
38     (\lambda a,b,K. y=a \to O=b \to
39         match K with [ (k a b p) \Rightarrow a ] = x)
40      ? ? ? H).
41  goal 16.*)
42  simplify. intros.
43  generalize in match H1.
44  rewrite < H2; rewrite < H3.intro.
45  rewrite > H4.autobatch library.
46 qed.
47
48 theorem t1: \forall x,y. sum x y O \to x = y.
49 intros.
50
51 (*
52 cut y=y \to O=O \to x = y.
53 apply Hcut.reflexivity. reflexivity.
54 apply (sum_ind ? (\lambda a,b,K. y=a \to O=b \to x=a) ? ? ? s).*)
55
56 (*apply (sum_ind ? (\lambda a,b,K. y = a \to O = b \to  x = a) ? ? ? s).*)
57 inversion s.
58 intros.simplify.
59 intros.
60 rewrite > H. rewrite < H2.  autobatch library.
61 qed.