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