matita/matita/contribs/lambda_delta/Ground_2/star.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 "basics/star.ma".
  16 include "Ground_2/xoa_props.ma".
  17
  18 (* PROPERTIES of RELATIONS **************************************************)
  19
  20 definition predicate: Type[0] → Type[0] ≝ λA. A → Prop.
  21
  22 definition Decidable: Prop → Prop ≝
  23    λR. R ∨ (R → False).
  24
  25 definition confluent: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
  26                       ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 →
  27                       ∃∃a. R2 a1 a & R1 a2 a.
  28
  29 definition transitive: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
  30                        ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 →
  31                        ∃∃a. R2 a1 a & R1 a a2.
  32
  33 lemma TC_strip1: ∀A,R1,R2. confluent A R1 R2 →
  34                  ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 →
  35                  ∃∃a. R2 a1 a & TC … R1 a2 a.
  36 #A #R1 #R2 #HR12 #a0 #a1 #H elim H -H a1
  37 [ #a1 #Ha01 #a2 #Ha02
  38   elim (HR12 … Ha01 … Ha02) -HR12 a0 /3/
  39 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
  40   elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20
  41   elim (HR12 … Ha1 … Ha0) -HR12 a /4/
  42 ]
  43 qed.
  44
  45 lemma TC_strip2: ∀A,R1,R2. confluent A R1 R2 →
  46                  ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a0 a1 →
  47                  ∃∃a. TC … R2 a1 a & R1 a2 a.
  48 #A #R1 #R2 #HR12 #a0 #a2 #H elim H -H a2
  49 [ #a2 #Ha02 #a1 #Ha01
  50   elim (HR12 … Ha01 … Ha02) -HR12 a0 /3/
  51 | #a #a2 #_ #Ha2 #IHa0 #a1 #Ha01
  52   elim (IHa0 … Ha01) -IHa0 Ha01 a0 #a0 #Ha10 #Ha0
  53   elim (HR12 … Ha0 … Ha2) -HR12 a /4/
  54 ]
  55 qed.
  56
  57 lemma TC_confluent: ∀A,R1,R2.
  58                     confluent A R1 R2 → confluent A (TC … R1) (TC … R2).
  59 #A #R1 #R2 #HR12 #a0 #a1 #H elim H -H a1
  60 [ #a1 #Ha01 #a2 #Ha02
  61   elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 a0 /3/
  62 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
  63   elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20
  64   elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 a /4/
  65 ]
  66 qed.
  67
  68 lemma TC_strap: ∀A. ∀R:relation A. ∀a1,a,a2.
  69                 R a1 a → TC … R a a2 → TC … R a1 a2.
  70 /3/ qed.
  71
  72 lemma TC_strap1: ∀A,R1,R2. transitive A R1 R2 →
  73                  ∀a1,a0. TC … R1 a1 a0 → ∀a2. R2 a0 a2 →
  74                  ∃∃a. R2 a1 a & TC … R1 a a2.
  75 #A #R1 #R2 #HR12 #a1 #a0 #H elim H -H a0
  76 [ #a0 #Ha10 #a2 #Ha02
  77   elim (HR12 … Ha10 … Ha02) -HR12 a0 /3/
  78 | #a #a0 #_ #Ha0 #IHa #a2 #Ha02
  79   elim (HR12 … Ha0 … Ha02) -HR12 a0 #a0 #Ha0 #Ha02
  80   elim (IHa … Ha0) -a /4/
  81 ]
  82 qed.
  83
  84 lemma TC_strap2: ∀A,R1,R2. transitive A R1 R2 →
  85                  ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a1 a0 →
  86                  ∃∃a. TC … R2 a1 a & R1 a a2.
  87 #A #R1 #R2 #HR12 #a0 #a2 #H elim H -H a2
  88 [ #a2 #Ha02 #a1 #Ha10
  89   elim (HR12 … Ha10 … Ha02) -HR12 a0 /3/
  90 | #a #a2 #_ #Ha02 #IHa #a1 #Ha10
  91   elim (IHa … Ha10) -a0 #a0 #Ha10 #Ha0
  92   elim (HR12 … Ha0 … Ha02) -HR12 a /4/
  93 ]
  94 qed.
  95
  96 lemma TC_transitive: ∀A,R1,R2.
  97                      transitive A R1 R2 → transitive A (TC … R1) (TC … R2).
  98 #A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0
  99 [ #a0 #Ha10 #a2 #Ha02
 100   elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 a0 /3/
 101 | #a #a0 #_ #Ha0 #IHa #a2 #Ha02
 102   elim (TC_strap2 … HR12 … Ha02 … Ha0) -HR12 a0 #a0 #Ha0 #Ha02
 103   elim (IHa … Ha0) -a /4/
 104 ]
 105 qed.
 106
 107 lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R).
 108 /2/ qed.
 109
 110 lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:predicate A.
 111                    P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) →
 112                    ∀a2. TC … R a1 a2 → P a2.
 113 #A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -Ha12 a2 /3/
 114 qed.
 115
 116 definition NF: ∀A. relation A → relation A → predicate A ≝
 117    λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2.
 118
 119 inductive SN (A) (R,S:relation A): predicate A ≝
 120 | SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → False) → SN A R S a2) → SN A R S a1
 121 .
 122
 123 lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a.
 124 #A #R #S #a1 #Ha1
 125 @SN_intro #a2 #HRa12 #HSa12
 126 elim (HSa12 ?) -HSa12 /2/
 127 qed.