]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/ng_elim.ma
init_copy init_match
[helm.git] / matita / 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 ]).