helm/software/matita/tests/ng_elim.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 ninductive nat: Type ≝
  16    O: nat
  17  | S: nat → nat.
  18
  19 nlet rec nat_rect (Q_: (∀ (x_1: (nat)).Type)) H_O H_S x_1 on x_1: (Q_ x_1) ≝
  20  (match x_1 with [O ⇒ (H_O) | (S x_2) ⇒ (H_S x_2 (nat_rect Q_ H_O H_S x_2))]).
  21
  22
  23 nlet rec nat_rec (Q: nat → Type) H_O H_S x_1 on x_1 : Q x_1 ≝
  24  match x_1 with
  25   [ O ⇒ H_O
  26   | S x_2 ⇒ H_S x_2 (nat_rec Q H_O H_S x_2)
  27   ].
  28
  29
  30 ninductive ord: Type ≝
  31    OO: ord
  32  | OS: ord → ord
  33  | OLim: (nat → ord) → ord.
  34
  35 nlet rec ord_rect (Q_: (∀ (x_3: (ord)).Type)) H_OO H_OS H_OLim x_3 on x_3: (Q_ x_3) ≝
  36  (match x_3 with [OO ⇒ (H_OO) | (OS x_4) ⇒ (H_OS x_4 (ord_rect Q_ H_OO H_OS H_OLim (x_4))) | (OLim x_6) ⇒ (H_OLim x_6 (λx_5.(ord_rect Q_ H_OO H_OS H_OLim (x_6 x_5))))]).
  37
  38
  39
  40 naxiom P: nat → Prop.
  41 naxiom p: ∀m. P m.
  42
  43 ninductive le (n:nat) (N: P n): ∀m:nat. P m → Type ≝
  44    len: le n N n (p n)
  45  | leS: ∀m,q.le n N m q → le n N (S m) (p (S m)).
  46
  47 nlet rec le_rect n N (Q_: (∀ m.(∀ x_4.(∀ (x_3: (le n N m x_4)).Type)))) H_len H_leS m x_4 x_3
  48  on x_3: (Q_ m x_4 x_3) ≝
  49 (match x_3 with [len ⇒ (H_len) | (leS m q x_5) ⇒ (H_leS m q x_5 (le_rect n N Q_ H_len H_leS ? ? x_5))]).
  50
  51 (*
  52 nlet rec le_rec' (n:nat) (Q: ∀D1:nat.∀D2: P D1. le n D1 D2 → Type) (p1: ?) (p2: ?) (D1:nat) (D2:P D1) (x: le n D1 D2) on x : Q D1 D2 x ≝
  53  match x with
  54   [ len ⇒ p1
  55   | leS m q A ⇒ p2 m q A (le_rec ? Q p1 p2 ?? A)
  56   ].
  57
  58 nlet rec le_rec (n:nat) (Q: ∀D1:nat.∀D2: P D1. le n D1 D2 → Type) (p1: ?) (p2: ?) (D1:nat) (D2:P D1) (x: le n D1 D2) on x : Q D1 D2 x ≝ ?.
  59  ## [ ncases x;
  60        ##[ #m; #q; #A; napply (p2 m q A (le_rec ? Q p1 p2 ?? A));
  61        ##| napply p1;
  62        ##]
  63  ## |##*: ## skip;
  64  ## ]
  65 nqed.*)
  66
  67 ninductive list (A:Type) : nat → Type ≝
  68    nil: list A O
  69  | cons: ∀n. A → list A n → list A (S n).
  70
  71 ninductive ii: Type ≝
  72  kk: list ii O → ii.
  73
  74 nlet rec ii_rect (Q_: (∀(x_16: ii).Type)) H_kknil H_kkcons x_16 on x_16: (Q_ x_16) ≝
  75  (match x_16 with
  76   [ kk x_17 ⇒ list_rect ii (λx_17.Q_ (kk x_17)) H_kknil (λw.H_kkcons w (ii_rect Q_ H_kknil H_kkcons w)) x_17 ]).