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.