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.