]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/ng_inversion.ma
splitting files
[helm.git] / matita / matita / tests / ng_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 include "logic/pts.ma".
16
17 (*naxiom foo : ?.
18 ##[##2:napply Prop;##|##skip]
19 nqed.*)
20
21 (*nlemma foo : ? → Prop.
22 ##[#a;*)
23
24 ninductive eq (A:Type[2]) (x:A) : A → Prop ≝
25 | refl : eq A x x.
26
27 ninductive nat : Type[0] ≝
28 | O : nat
29 | S : nat → nat.
30
31 (*ninductive pippo : nat → Type[1] ≝
32 | pO  : pippo O
33 | pSS : ∀n.pippo n → pippo (S (S n)).
34 *)
35
36 ninductive list (A:Type[0]) : Type[0] ≝
37 | nil  : list A
38 | cons : A → list A → list A.
39
40 ninductive False : Prop ≝ .
41
42 naxiom daemon : False.
43
44 ninductive in_list (A:Type[0]) : A → list A → Prop ≝
45 | in_list_head : ∀x,l.in_list A x (cons A x l)
46 | in_list_cons : ∀x,y,l.in_list A x l → in_list A x (cons A y l).
47
48 ninductive ppippo : nat → Prop ≝
49 | ppO : ppippo O
50 | ppSS : ∀n.ppippo n → ppippo  (S (S n)).
51
52 ndefinition Not : Prop → Prop ≝ λP.P → False.
53
54 ninductive Typ : Type[0] ≝
55 | TVar : nat → Typ
56 | TFree : nat → Typ
57 | Top : Typ
58 | Arrow : Typ → Typ → Typ
59 | Forall : Typ → Typ → Typ.
60
61 ninductive bool : Type[0] ≝
62 | true : bool
63 | false : bool.
64
65 nrecord bound : Type ≝ { 
66                           istype : bool;    (* is subtyping bound? *)
67                           name   : nat ;    (* name *)
68                           btype  : Typ      (* type to which the name is bound *)
69                         }.
70                         
71 nlet rec eqb m n ≝
72  match m with
73  [ O ⇒ match n with
74   [ O ⇒ true
75   | S q ⇒ false ]
76  | S p ⇒ match n with
77   [ O ⇒ false
78   | S q ⇒ eqb p q ]].  
79                
80 (*** Various kinds of substitution, not all will be used probably ***)
81
82 (* substitutes i-th dangling index in type T with type U *)
83 nlet rec subst_type_nat T U i ≝
84     match T with
85     [ TVar n ⇒ match eqb n i with
86       [ true ⇒ U
87       | false ⇒ T]
88     | TFree X ⇒ T
89     | Top ⇒ T
90     | Arrow T1 T2 ⇒ Arrow (subst_type_nat T1 U i) (subst_type_nat T2 U i)
91     | Forall T1 T2 ⇒ Forall (subst_type_nat T1 U i) (subst_type_nat T2 U (S i)) ].
92
93 nlet rec map A B f (l : list A) on l : list B ≝
94   match l with [ nil ⇒ nil ? | cons x tl ⇒ cons ? (f x) (map ?? f tl)].
95   
96 nlet rec foldr (A,B:Type[0]) f b (l : list A) on l : B ≝  
97   match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr A B f b l)].
98    
99 ndefinition length ≝ λT:Type.λl:list T.foldr T nat (λx,c.S c) O l.
100
101 ndefinition filter \def 
102   \lambda T:Type.\lambda l:list T.\lambda p:T \to bool.
103   foldr T (list T) 
104     (\lambda x,l0.match (p x) with [ true => cons ? x l0 | false => l0]) (nil ?) l.
105
106
107 (*** definitions about lists ***)
108
109 ndefinition filter_types : list bound → list bound ≝
110   λG.(filter ? G (λB.match B with [mk_bound B X T ⇒ B])).
111
112 ndefinition fv_env : list bound → list nat ≝
113   λG.(map ? ? (λb.match b with [mk_bound B X T ⇒ X]) (filter_types G)).
114
115 nlet rec append A (l1: list A) l2 on l1 :=
116   match l1 with
117   [ nil => l2
118   | (cons hd tl) => cons ? hd (append A tl l2) ].
119
120 nlet rec fv_type T ≝
121   match T with
122     [TVar n ⇒ nil ?
123     |TFree x ⇒ cons ? x (nil ?)
124     |Top ⇒ nil ?
125     |Arrow U V ⇒ append ? (fv_type U) (fv_type V)
126     |Forall U V ⇒ append ? (fv_type U) (fv_type V)].
127
128 (*** Type Well-Formedness judgement ***)
129
130 ninductive WFType : list bound → Typ → Prop ≝
131   | WFT_TFree : ∀X,G.in_list ? X (fv_env G) → WFType G (TFree X)
132   | WFT_Top : ∀G.WFType G Top
133   | WFT_Arrow : ∀G,T,U.WFType G T → WFType G U → WFType G (Arrow T U)
134   | WFT_Forall : ∀G,T,U.WFType G T →
135                    (∀X:nat.
136                     (Not (in_list ? X (fv_env G))) →
137                     (Not (in_list ? X (fv_type U))) →
138                     (WFType (cons ? (mk_bound true X T)  G)
139                      (subst_type_nat U (TFree X) O))) → 
140                  (WFType G (Forall T U)).
141
142 ninductive WFEnv : list bound → Prop ≝
143   | WFE_Empty : WFEnv (nil ?)
144   | WFE_cons : ∀B,X,T,G.WFEnv G → Not (in_list ? X (fv_env G)) →
145                   WFType G T → WFEnv (cons ? (mk_bound B X T) G).
146             
147 (*** Subtyping judgement ***)              
148 ninductive JSubtype : list bound → Typ → Typ → Prop ≝
149   | SA_Top : ∀G,T.WFEnv G → WFType G T → JSubtype G T Top
150   | SA_Refl_TVar : ∀G,X.WFEnv G → in_list ? X (fv_env G) 
151                    → JSubtype G (TFree X) (TFree X)
152   | SA_Trans_TVar : ∀G,X,T,U.in_list ? (mk_bound true X U) G →
153                     JSubtype G U T → JSubtype G (TFree X) T
154   | SA_Arrow : ∀G,S1,S2,T1,T2. JSubtype G T1 S1 → JSubtype G S2 T2 → 
155                JSubtype G (Arrow S1 S2) (Arrow T1 T2)
156   | SA_All : ∀G,S1,S2,T1,T2. JSubtype G T1 S1 →
157              (∀X.Not (in_list ? X (fv_env G)) →
158                JSubtype (cons ? (mk_bound true X T1) G) 
159                 (subst_type_nat S2 (TFree X) O) (subst_type_nat T2 (TFree X) O)) →
160              JSubtype G (Forall S1 S2) (Forall T1 T2).
161
162 inductive jmeq (A:Type) (a:A) : ∀B:Type.B → Prop ≝
163 | refl_jmeq : jmeq A a A a. 
164
165 ninverter JS_indinv for JSubtype (%?%).
166
167 (*** ***)
168
169 ninverter dasd for pippo (?) : Type.
170
171 inductive nat : Type ≝
172 | O : nat 
173 | S : nat → nat.
174
175 inductive ppippo : nat → Prop ≝
176 | ppO : ppippo O
177 | ppSS : ∀n.ppippo n → ppippo  (S (S n)).
178
179 nlemma pippo_inv : ∀x.∀P:? → Prop.? → ? → ? → P x.
180 ##[ (* ok, qui bisogna selezionare la meta del goal *)
181    #x;#P;#H1;#H2;#H;
182    napply ((λHcut:(eqn ? x x → P x).?) ?);
183    ##[(* questa e` la meta cut *)
184       nletin p ≝ pippo_ind;
185       napply (pippo_ind (λy,p.eqn ? x y → P y) H1 H2 … H);
186       (* [ * cons 1 *
187          napply H1
188       | * cons 2 *
189          napply H2
190       | * inductive term *
191          napply H ] *)
192    ##| napply Hcut; napply nrefl_eq]
193    ##]
194    ##skip;
195 nqed.