matita/matita/lib/pts_dummy_new/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 → T      (* dummy term, type *)
  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 normalize //
  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
  47 (* neutral terms
  48    secondo me questa definzione non va qui, comunque la
  49    estendo al caso dummy *)
  50 inductive neutral: T → Prop ≝
  51    | neutral_sort: ∀n.neutral (Sort n)
  52    | neutral_rel: ∀i.neutral (Rel i)
  53    | neutral_app: ∀M,N.neutral (App M N)
  54    | neutral_dummy: ∀M,N.neutral (D M N)
  55 .