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 Decidable: Prop → Prop ≝ λR. R ∨ (R → False).
  21
  22 definition confluent2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
  23                        ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 →
  24                        ∃∃a. R2 a1 a & R1 a2 a.
  25
  26 definition transitive2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
  27                         ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 →
  28                         ∃∃a. R2 a1 a & R1 a a2.
  29
  30 lemma TC_strip1: ∀A,R1,R2. confluent2 A R1 R2 →
  31                  ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 →
  32                  ∃∃a. R2 a1 a & TC … R1 a2 a.
  33 #A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1
  34 [ #a1 #Ha01 #a2 #Ha02
  35   elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3/
  36 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
  37   elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20
  38   elim (HR12 … Ha1 … Ha0) -HR12 -a /4 width=3/
  39 ]
  40 qed.
  41
  42 lemma TC_strip2: ∀A,R1,R2. confluent2 A R1 R2 →
  43                  ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a0 a1 →
  44                  ∃∃a. TC … R2 a1 a & R1 a2 a.
  45 #A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2
  46 [ #a2 #Ha02 #a1 #Ha01
  47   elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3/
  48 | #a #a2 #_ #Ha2 #IHa0 #a1 #Ha01
  49   elim (IHa0 … Ha01) -a0 #a0 #Ha10 #Ha0
  50   elim (HR12 … Ha0 … Ha2) -HR12 -a /4 width=3/
  51 ]
  52 qed.
  53
  54 lemma TC_confluent2: ∀A,R1,R2.
  55                      confluent2 A R1 R2 → confluent2 A (TC … R1) (TC … R2).
  56 #A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1
  57 [ #a1 #Ha01 #a2 #Ha02
  58   elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 -a0 /3 width=3/
  59 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
  60   elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20
  61   elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 -a /4 width=3/
  62 ]
  63 qed.
  64
  65 lemma TC_strap1: ∀A,R1,R2. transitive2 A R1 R2 →
  66                  ∀a1,a0. TC … R1 a1 a0 → ∀a2. R2 a0 a2 →
  67                  ∃∃a. R2 a1 a & TC … R1 a a2.
  68 #A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0
  69 [ #a0 #Ha10 #a2 #Ha02
  70   elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3/
  71 | #a #a0 #_ #Ha0 #IHa #a2 #Ha02
  72   elim (HR12 … Ha0 … Ha02) -HR12 -a0 #a0 #Ha0 #Ha02
  73   elim (IHa … Ha0) -a /4 width=3/
  74 ]
  75 qed.
  76
  77 lemma TC_strap2: ∀A,R1,R2. transitive2 A R1 R2 →
  78                  ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a1 a0 →
  79                  ∃∃a. TC … R2 a1 a & R1 a a2.
  80 #A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2
  81 [ #a2 #Ha02 #a1 #Ha10
  82   elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3/
  83 | #a #a2 #_ #Ha02 #IHa #a1 #Ha10
  84   elim (IHa … Ha10) -a0 #a0 #Ha10 #Ha0
  85   elim (HR12 … Ha0 … Ha02) -HR12 -a /4 width=3/
  86 ]
  87 qed.
  88
  89 lemma TC_transitive2: ∀A,R1,R2.
  90                       transitive2 A R1 R2 → transitive2 A (TC … R1) (TC … R2).
  91 #A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0
  92 [ #a0 #Ha10 #a2 #Ha02
  93   elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 -a0 /3 width=3/
  94 | #a #a0 #_ #Ha0 #IHa #a2 #Ha02
  95   elim (TC_strap2 … HR12 … Ha02 … Ha0) -HR12 -a0 #a0 #Ha0 #Ha02
  96   elim (IHa … Ha0) -a /4 width=3/
  97 ]
  98 qed.
  99
 100 definition NF: ∀A. relation A → relation A → predicate A ≝
 101    λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2.
 102
 103 inductive SN (A) (R,S:relation A): predicate A ≝
 104 | SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → False) → SN A R S a2) → SN A R S a1
 105 .
 106
 107 lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a.
 108 #A #R #S #a1 #Ha1
 109 @SN_intro #a2 #HRa12 #HSa12
 110 elim (HSa12 ?) -HSa12 /2 width=1/
 111 qed.