matita/matita/lib/pts_dummy/convertibility.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 "pts_dummy/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
  25 inductive conv1 : T →T → Prop ≝
  26   | cbeta: ∀P,M,N. conv1 (App (Lambda P M) N) (M[0 ≝ N])
  27   | cappl: ∀M,M1,N. conv1 M M1 → conv1 (App M N) (App M1 N)
  28   | cappr: ∀M,N,N1. conv1 N N1 → conv1 (App M N) (App M N1)
  29   | claml: ∀M,M1,N. conv1 M M1 → conv1 (Lambda M N) (Lambda M1 N)
  30   | clamr: ∀M,N,N1. conv1 N N1 → conv1 (Lambda M N) (Lambda M N1)
  31   | cprodl: ∀M,M1,N. conv1 M M1 → conv1 (Prod M N) (Prod M1 N)
  32   | cprodr: ∀M,N,N1. conv1 N N1 → conv1 (Prod M N) (Prod M N1)
  33   | cd: ∀M,M1. conv1 (D M) (D M1).
  34
  35 definition conv ≝ star … conv1.
  36
  37 lemma red_to_conv1: ∀M,N. red M N → conv1 M N.
  38 #M #N #redMN (elim redMN) /2/
  39 qed.
  40
  41 inductive d_eq : T →T → Prop ≝
  42   | same: ∀M. d_eq M M
  43   | ed: ∀M,M1. d_eq (D M) (D M1)
  44   | eapp: ∀M1,M2,N1,N2. d_eq M1 M2 → d_eq N1 N2 →
  45       d_eq (App M1 N1) (App M2 N2)
  46   | elam: ∀M1,M2,N1,N2. d_eq M1 M2 → d_eq N1 N2 →
  47       d_eq (Lambda M1 N1) (Lambda M2 N2)
  48   | eprod: ∀M1,M2,N1,N2. d_eq M1 M2 → d_eq N1 N2 →
  49       d_eq (Prod M1 N1) (Prod M2 N2).
  50
  51 lemma conv1_to_deq: ∀M,N. conv1 M N → red M N ∨ d_eq M N.
  52 #M #N #coMN (elim coMN)
  53   [#P #B #C %1 //
  54   |#P #M1 #N1 #coPM1 * [#redP %1 /2/ | #eqPM1 %2 /3/]
  55   |#P #M1 #N1 #coPM1 * [#redP %1 /2/ | #eqPM1 %2 /3/]
  56   |#P #M1 #N1 #coPM1 * [#redP %1 /2/ | #eqPM1 %2 /3/]
  57   |#P #M1 #N1 #coPM1 * [#redP %1 /2/ | #eqPM1 %2 /3/]
  58   |#P #M1 #N1 #coPM1 * [#redP %1 /2/ | #eqPM1 %2 /3/]
  59   |#P #M1 #N1 #coPM1 * [#redP %1 /2/ | #eqPM1 %2 /3/]
  60   |#P #M1 %2 //
  61   ]
  62 qed.
  63
  64 (* FG: THIS IS NOT COMPLETE
  65 theorem main1: ∀M,N. conv M N →
  66   ∃P,Q. star … red M P ∧ star … red N Q ∧ d_eq P Q.
  67 #M #N #coMN (elim coMN)
  68   [#B #C #rMB #convBC * #P1 * #Q1 * * #redMP1 #redBQ1
  69    #deqP1Q1 (cases (conv_to_deq … convBC))
  70     [
  71   |@(ex_intro … M) @(ex_intro … M) % // % //
  72   ]
  73 *)
  74 *)