]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/lambda/terms.ma
cube.ma: some pts specifications of the lambda-cube
[helm.git] / matita / matita / lib / lambda / terms.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department of the University of Bologna, Italy.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  This file is distributed under the terms of the 
8     \   /  GNU General Public License Version 2        
9      \ /      
10       V_______________________________________________________________ *)
11
12 include "basics/list.ma".
13 include "lambda/lambda_notation.ma".
14
15 inductive T : Type[0] ≝
16   | Sort: nat → T     (* starts from 0 *)
17   | Rel: nat → T      (* starts from 0 *)
18   | App: T → T → T    (* function, argument *)
19   | Lambda: T → T → T (* type, body *)
20   | Prod: T → T → T   (* type, body *)
21   | D: T → T          (* dummifier *)
22 .
23
24 (* Appl F l generalizes App applying F to a list of arguments
25  * The head of l is applied first
26  *)
27 let rec Appl F l on l ≝ match l with 
28    [ nil ⇒ F
29    | cons A D ⇒ Appl (App F A) D  
30    ].
31
32 lemma appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
33 #N #l elim l -l // #hd #tl #IHl #M >IHl //
34 qed.
35
36 (*
37 let rec is_dummy t ≝ match t with
38    [ Sort _     ⇒ false
39    | Rel _      ⇒ false
40    | App M _    ⇒ is_dummy M
41    | Lambda _ M ⇒ is_dummy M
42    | Prod _ _   ⇒ false       (* not so sure yet *)
43    | D _        ⇒ true
44    ].
45 *)
46 (* nautral terms *)
47 inductive neutral: T → Prop ≝
48    | neutral_sort: ∀n.neutral (Sort n)
49    | neutral_rel: ∀i.neutral (Rel i)
50    | neutral_app: ∀M,N.neutral (App M N)
51 .