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 naxiom P: nat → Prop.
  30 naxiom p: ∀m. P m.
  31
  32 ninductive le (n:nat) (N: P n): ∀m:nat. P m → Type ≝
  33    len: le n N n (p n)
  34  | leS: ∀m,q.le n N m q → le n N (S m) (p (S m)).
  35
  36 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
  37  on x_3: (Q_ m x_4 x_3) ≝
  38 (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))]).
  39
  40
  41
  42 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 ≝
  43  match x with
  44   [ len ⇒ p1
  45   | leS m q A ⇒ p2 m q A (le_rec ? Q p1 p2 ?? A)
  46   ].
  47
  48 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 ≝ ?.
  49  ## [ ncases x;
  50        ##[ #m; #q; #A; napply (p2 m q A (le_rec ? Q p1 p2 ?? A));
  51        ##| napply p1;
  52        ##]
  53  ## |##*: ## skip;
  54  ## ]
  55 nqed.