matita/matita/lib/lambda/reduction.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 "lambda/par_reduction.ma".
  13
  14 (*
  15 inductive T : Type[0] ≝
  16   | Sort: nat → T
  17   | Rel: nat → T
  18   | App: T → T → T
  19   | Lambda: T → T → T (* type, body *)
  20   | Prod: T → T → T (* type, body *)
  21   | D: T →T
  22 . *)
  23
  24 inductive red : T →T → Prop ≝
  25   | rbeta: ∀P,M,N. red (App (Lambda P M) N) (M[0 ≝ N])
  26   | rdapp: ∀M,N. red (App (D M) N) (D (App M N))
  27   | rdlam: ∀M,N. red (Lambda M (D N)) (D (Lambda M N))
  28   | rappl: ∀M,M1,N. red M M1 → red (App M N) (App M1 N)
  29   | rappr: ∀M,N,N1. red N N1 → red (App M N1) (App M N1)
  30   | rlaml: ∀M,M1,N. red M M1 → red (Lambda M N) (Lambda M1 N)
  31   | rlamr: ∀M,N,N1. red N N1 → red(Lambda M N1) (Lambda M N1)
  32   | rprodl: ∀M,M1,N. red M M1 → red (Prod M N) (Prod M1 N)
  33   | rprodr: ∀M,N,N1. red N N1 → red (Prod M N1) (Prod M N1)
  34   | d: ∀M,M1. red M M1 → red (D M) (D M1).
  35
  36 lemma red_to_pr: ∀M,N. red M N → pr M N.
  37 #M #N #redMN (elim redMN) /2/
  38 qed.
  39
  40
  41
  42
  43
  44