1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basics/star.ma".
16 include "Ground_2/xoa_props.ma".
18 (* PROPERTIES of RELATIONS **************************************************)
20 definition Decidable: Prop → Prop ≝
23 definition confluent: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
24 ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 →
25 ∃∃a. R2 a1 a & R1 a2 a.
27 definition transitive: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
28 ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 →
29 ∃∃a. R2 a1 a & R1 a a2.
31 lemma TC_strip1: ∀A,R1,R2. confluent A R1 R2 →
32 ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 →
33 ∃∃a. R2 a1 a & TC … R1 a2 a.
34 #A #R1 #R2 #HR12 #a0 #a1 #H elim H -H a1
36 elim (HR12 … Ha01 … Ha02) -HR12 a0 /3/
37 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
38 elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20
39 elim (HR12 … Ha1 … Ha0) -HR12 a /4/
43 lemma TC_strip2: ∀A,R1,R2. confluent A R1 R2 →
44 ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a0 a1 →
45 ∃∃a. TC … R2 a1 a & R1 a2 a.
46 #A #R1 #R2 #HR12 #a0 #a2 #H elim H -H a2
48 elim (HR12 … Ha01 … Ha02) -HR12 a0 /3/
49 | #a #a2 #_ #Ha2 #IHa0 #a1 #Ha01
50 elim (IHa0 … Ha01) -IHa0 Ha01 a0 #a0 #Ha10 #Ha0
51 elim (HR12 … Ha0 … Ha2) -HR12 a /4/
55 lemma TC_confluent: ∀A,R1,R2.
56 confluent A R1 R2 → confluent A (TC … R1) (TC … R2).
57 #A #R1 #R2 #HR12 #a0 #a1 #H elim H -H a1
59 elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 a0 /3/
60 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
61 elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20
62 elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 a /4/
66 lemma TC_strap: ∀A. ∀R:relation A. ∀a1,a,a2.
67 R a1 a → TC … R a a2 → TC … R a1 a2.
70 lemma TC_strap1: ∀A,R1,R2. transitive A R1 R2 →
71 ∀a1,a0. TC … R1 a1 a0 → ∀a2. R2 a0 a2 →
72 ∃∃a. R2 a1 a & TC … R1 a a2.
73 #A #R1 #R2 #HR12 #a1 #a0 #H elim H -H a0
75 elim (HR12 … Ha10 … Ha02) -HR12 a0 /3/
76 | #a #a0 #_ #Ha0 #IHa #a2 #Ha02
77 elim (HR12 … Ha0 … Ha02) -HR12 a0 #a0 #Ha0 #Ha02
78 elim (IHa … Ha0) -a /4/
82 lemma TC_strap2: ∀A,R1,R2. transitive A R1 R2 →
83 ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a1 a0 →
84 ∃∃a. TC … R2 a1 a & R1 a a2.
85 #A #R1 #R2 #HR12 #a0 #a2 #H elim H -H a2
87 elim (HR12 … Ha10 … Ha02) -HR12 a0 /3/
88 | #a #a2 #_ #Ha02 #IHa #a1 #Ha10
89 elim (IHa … Ha10) -a0 #a0 #Ha10 #Ha0
90 elim (HR12 … Ha0 … Ha02) -HR12 a /4/
94 lemma TC_transitive: ∀A,R1,R2.
95 transitive A R1 R2 → transitive A (TC … R1) (TC … R2).
96 #A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0
98 elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 a0 /3/
99 | #a #a0 #_ #Ha0 #IHa #a2 #Ha02
100 elim (TC_strap2 … HR12 … Ha02 … Ha0) -HR12 a0 #a0 #Ha0 #Ha02
101 elim (IHa … Ha0) -a /4/
105 lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R).
108 lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:A→Prop.
109 P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) →
110 ∀a2. TC … R a1 a2 → P a2.
111 #A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -Ha12 a2 /3/
114 definition NF: ∀A. relation A → relation A → A → Prop ≝
115 λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2.
117 inductive SN (A) (R,S:relation A): A → Prop ≝
118 | SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → False) → SN A R S a2) → SN A R S a1
121 lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a.
123 @SN_intro #a2 #HRa12 #HSa12
124 elim (HSa12 ?) -HSa12 /2/