]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/nelim-userspace.ma
splitting files
[helm.git] / matita / matita / tests / nelim-userspace.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 "hints_declaration.ma".
16
17 nrecord eliminator (P_ : Prop) (T_ : Type[1]) : Type[1] ≝ {
18   indty : Type[0];
19   elimP : indty → P_;
20   elimT : indty → T_
21 }.
22
23 notation "\elim term 90 x term 90 P" non associative with precedence 90 
24 for @{'elim ?? ? $x … $P … $x}.
25 interpretation "elimP" 'elim = elimP.
26 interpretation "elimT" 'elim = elimT.
27
28 ninductive nat : Type[0] ≝ O : nat | S : nat → nat.
29
30 ndefinition eP ≝ mk_eliminator ?? nat (λ_.nat_ind) (λ_.nat_rect_Type0).
31
32 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
33 unification hint 0 ≔;
34   X ≟ eP
35 (*-----------------------------------------*) ⊢
36   indty ?? X ≡ nat.
37   
38 ninductive list (A : Type[0]) : nat → Type[0] ≝ 
39 | nil : list A O
40 | cons : ∀n.A → list A n → list A (S n).
41
42 ndefinition eL ≝ λA,n.
43   mk_eliminator ?? (list A n) (λ_.list_ind A) (λ_.list_rect_Type0 A).
44
45 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
46 unification hint 0 ≔ A,n;
47   X ≟ eL A n
48 (*-----------------------------------------*) ⊢
49   indty ?? X ≡ list A n.  
50
51 naxiom A : ∀n1,n2.∀l1:list nat n1.∀l2:list nat n2.Prop.
52
53 nlemma xxx : ∀n.∀x:list nat n.A ?? x x.
54 #n; #l;
55 napply (\elim l (λd,y.A ?? y l)); 
56
57
58 ##[ ##| #len e l1 Pl1;
59 napply ((\elim ?? ? x) … x); #;#[ napply eP]
60
61
62 nrecord eliminator (indty : Type[0]) 
63                    (s : Type[2])    
64                    (t : Type[1]) : Type[2] ≝ {
65   elimp : t
66 }.
67
68
69 ndefinition P :
70   ?
71 ≝  
72   λity,s,t.λR : eliminator ity s t. λG:s.
73    match R with [ mk_eliminator _ ⇒ G].
74
75 ninductive nat : Type[0] ≝ O : nat | S : nat → nat.
76
77 ndefinition eP := mk_eliminator nat Prop    ? nat_ind.
78 ndefinition eT := mk_eliminator nat Type[0] ? nat_rect_Type0.
79
80 unification hint 0 ≔ G;
81   X ≟ eP
82 (*-----------------------------------------*) ⊢
83   P nat Prop ? X G ≡ G.
84   (*
85 unification hint 0 ≔ G;
86   X ≟ eT
87 (*-----------------------------------------*) ⊢
88   P nat Type[0] ? X G ≡ G.
89   *)
90
91 nlemma A : nat.
92 napply (
93
94 ndefinition elim_gen : 
95   ∀ity:Type[0].∀s,t.∀x:ity.
96     ∀e:eliminator ity s t.∀G.P ity s t e G 
97
98   λity,s,t,x,e,G.elimp ??? e x.