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 "ground_2/notation/relations/funexteq_2.ma".
16 include "ground_2/relocation/rtmap.ma".
18 (* RELOCATION MAP ***********************************************************)
20 coinductive eq: relation rtmap ≝
21 | eq_push: ∀f1,f2,g1,g2. eq f1 f2 → ↑f1 = g1 → ↑f2 = g2 → eq g1 g2
22 | eq_next: ∀f1,f2,g1,g2. eq f1 f2 → ⫯f1 = g1 → ⫯f2 = g2 → eq g1 g2
25 interpretation "extensional equivalence (rtmap)"
26 'FunExtEq f1 f2 = (eq f1 f2).
28 definition eq_repl (R:relation …) ≝
29 ∀f1,f2. f1 ≗ f2 → R f1 f2.
31 definition eq_repl_back (R:predicate …) ≝
32 ∀f1. R f1 → ∀f2. f1 ≗ f2 → R f2.
34 definition eq_repl_fwd (R:predicate …) ≝
35 ∀f1. R f1 → ∀f2. f2 ≗ f1 → R f2.
37 (* Basic properties *********************************************************)
39 corec lemma eq_refl: reflexive … eq.
40 #f cases (pn_split f) *
41 #g #Hg [ @(eq_push … Hg Hg) | @(eq_next … Hg Hg) ] -Hg //
44 corec lemma eq_sym: symmetric … eq.
46 #f1 #f2 #g1 #g2 #Hf #H1 #H2
47 [ @(eq_push … H2 H1) | @(eq_next … H2 H1) ] -g2 -g1 /2 width=1 by/
50 lemma eq_repl_sym: ∀R. eq_repl_back R → eq_repl_fwd R.
51 /3 width=3 by eq_sym/ qed-.
53 (* Basic inversion lemmas ***************************************************)
55 lemma eq_inv_px: ∀g1,g2. g1 ≗ g2 → ∀f1. ↑f1 = g1 →
56 ∃∃f2. f1 ≗ f2 & ↑f2 = g2.
58 #f1 #f2 #g1 #g2 #Hf * * -g1 -g2
60 [ lapply (injective_push … H) -H /2 width=3 by ex2_intro/
61 | elim (discr_push_next … H)
65 lemma eq_inv_nx: ∀g1,g2. g1 ≗ g2 → ∀f1. ⫯f1 = g1 →
66 ∃∃f2. f1 ≗ f2 & ⫯f2 = g2.
68 #f1 #f2 #g1 #g2 #Hf * * -g1 -g2
70 [ elim (discr_next_push … H)
71 | lapply (injective_next … H) -H /2 width=3 by ex2_intro/
75 lemma eq_inv_xp: ∀g1,g2. g1 ≗ g2 → ∀f2. ↑f2 = g2 →
76 ∃∃f1. f1 ≗ f2 & ↑f1 = g1.
78 #f1 #f2 #g1 #g2 #Hf * * -g1 -g2
80 [ lapply (injective_push … H) -H /2 width=3 by ex2_intro/
81 | elim (discr_push_next … H)
85 lemma eq_inv_xn: ∀g1,g2. g1 ≗ g2 → ∀f2. ⫯f2 = g2 →
86 ∃∃f1. f1 ≗ f2 & ⫯f1 = g1.
88 #f1 #f2 #g1 #g2 #Hf * * -g1 -g2
90 [ elim (discr_next_push … H)
91 | lapply (injective_next … H) -H /2 width=3 by ex2_intro/
95 (* Advanced inversion lemmas ************************************************)
97 lemma eq_inv_pp: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ≗ f2.
98 #g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_px … H … H1) -g1
100 #H lapply (injective_push … H) -H //
103 lemma eq_inv_nn: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ≗ f2.
104 #g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_nx … H … H1) -g1
106 #H lapply (injective_next … H) -H //
109 lemma eq_inv_pn: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → ⊥.
110 #g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_px … H … H1) -g1
112 #H elim (discr_next_push … H)
115 lemma eq_inv_np: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → ⊥.
116 #g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_nx … H … H1) -g1
118 #H elim (discr_push_next … H)
121 lemma eq_inv_gen: ∀f1,f2. f1 ≗ f2 →
122 (∃∃g1,g2. g1 ≗ g2 & ↑g1 = f1 & ↑g2 = f2) ∨
123 ∃∃g1,g2. g1 ≗ g2 & ⫯g1 = f1 & ⫯g2 = f2.
124 #f1 elim (pn_split f1) * #g1 #H1 #f2 #Hf
125 [ elim (eq_inv_px … Hf … H1) -Hf /3 width=5 by or_introl, ex3_2_intro/
126 | elim (eq_inv_nx … Hf … H1) -Hf /3 width=5 by or_intror, ex3_2_intro/
130 (* Main properties **********************************************************)
132 corec theorem eq_trans: Transitive … eq.
134 #f1 #f #g1 #g #Hf1 #H1 #H #f2 #Hf2
135 [ cases (eq_inv_px … Hf2 … H) | cases (eq_inv_nx … Hf2 … H) ] -g
136 /3 width=5 by eq_push, eq_next/
139 theorem eq_canc_sn: ∀f2. eq_repl_back (λf. f ≗ f2).
140 /3 width=3 by eq_trans, eq_sym/ qed-.
142 theorem eq_canc_dx: ∀f1. eq_repl_fwd (λf. f1 ≗ f).
143 /3 width=3 by eq_trans, eq_sym/ qed-.