(* *)
(**************************************************************************)
-include "ground_2/notation/relations/funexteq_2.ma".
+include "ground_2/notation/relations/ideq_2.ma".
include "ground_2/relocation/rtmap.ma".
(* RELOCATION MAP ***********************************************************)
coinductive eq: relation rtmap ≝
-| eq_push: â\88\80f1,f2,g1,g2. eq f1 f2 â\86\92 â\86\91f1 = g1 â\86\92 â\86\91f2 = g2 → eq g1 g2
-| eq_next: â\88\80f1,f2,g1,g2. eq f1 f2 â\86\92 ⫯f1 = g1 â\86\92 ⫯f2 = g2 → eq g1 g2
+| eq_push: â\88\80f1,f2,g1,g2. eq f1 f2 â\86\92 ⫯f1 = g1 â\86\92 ⫯f2 = g2 → eq g1 g2
+| eq_next: â\88\80f1,f2,g1,g2. eq f1 f2 â\86\92 â\86\91f1 = g1 â\86\92 â\86\91f2 = g2 → eq g1 g2
.
interpretation "extensional equivalence (rtmap)"
- 'FunExtEq f1 f2 = (eq f1 f2).
+ 'IdEq f1 f2 = (eq f1 f2).
definition eq_repl (R:relation …) ≝
- â\88\80f1,f2. f1 â\89\97 f2 → R f1 f2.
+ â\88\80f1,f2. f1 â\89¡ f2 → R f1 f2.
definition eq_repl_back (R:predicate …) ≝
- â\88\80f1. R f1 â\86\92 â\88\80f2. f1 â\89\97 f2 → R f2.
+ â\88\80f1. R f1 â\86\92 â\88\80f2. f1 â\89¡ f2 → R f2.
definition eq_repl_fwd (R:predicate …) ≝
- â\88\80f1. R f1 â\86\92 â\88\80f2. f2 â\89\97 f1 → R f2.
+ â\88\80f1. R f1 â\86\92 â\88\80f2. f2 â\89¡ f1 → R f2.
(* Basic properties *********************************************************)
(* Basic inversion lemmas ***************************************************)
-lemma eq_inv_px: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f1. â\86\91f1 = g1 →
- â\88\83â\88\83f2. f1 â\89\97 f2 & â\86\91f2 = g2.
+lemma eq_inv_px: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f1. ⫯f1 = g1 →
+ â\88\83â\88\83f2. f1 â\89¡ f2 & ⫯f2 = g2.
#g1 #g2 * -g1 -g2
#f1 #f2 #g1 #g2 #Hf * * -g1 -g2
#x1 #H
]
qed-.
-lemma eq_inv_nx: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f1. ⫯f1 = g1 →
- â\88\83â\88\83f2. f1 â\89\97 f2 & ⫯f2 = g2.
+lemma eq_inv_nx: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f1. â\86\91f1 = g1 →
+ â\88\83â\88\83f2. f1 â\89¡ f2 & â\86\91f2 = g2.
#g1 #g2 * -g1 -g2
#f1 #f2 #g1 #g2 #Hf * * -g1 -g2
#x1 #H
]
qed-.
-lemma eq_inv_xp: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f2. â\86\91f2 = g2 →
- â\88\83â\88\83f1. f1 â\89\97 f2 & â\86\91f1 = g1.
+lemma eq_inv_xp: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f2. ⫯f2 = g2 →
+ â\88\83â\88\83f1. f1 â\89¡ f2 & ⫯f1 = g1.
#g1 #g2 * -g1 -g2
#f1 #f2 #g1 #g2 #Hf * * -g1 -g2
#x2 #H
]
qed-.
-lemma eq_inv_xn: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f2. ⫯f2 = g2 →
- â\88\83â\88\83f1. f1 â\89\97 f2 & ⫯f1 = g1.
+lemma eq_inv_xn: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f2. â\86\91f2 = g2 →
+ â\88\83â\88\83f1. f1 â\89¡ f2 & â\86\91f1 = g1.
#g1 #g2 * -g1 -g2
#f1 #f2 #g1 #g2 #Hf * * -g1 -g2
#x2 #H
(* Advanced inversion lemmas ************************************************)
-lemma eq_inv_pp: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f1,f2. â\86\91f1 = g1 â\86\92 â\86\91f2 = g2 â\86\92 f1 â\89\97 f2.
+lemma eq_inv_pp: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f1,f2. ⫯f1 = g1 â\86\92 ⫯f2 = g2 â\86\92 f1 â\89¡ f2.
#g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_px … H … H1) -g1
#x2 #Hx2 * -g2
#H lapply (injective_push … H) -H //
qed-.
-lemma eq_inv_nn: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f1,f2. ⫯f1 = g1 â\86\92 ⫯f2 = g2 â\86\92 f1 â\89\97 f2.
+lemma eq_inv_nn: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f1,f2. â\86\91f1 = g1 â\86\92 â\86\91f2 = g2 â\86\92 f1 â\89¡ f2.
#g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_nx … H … H1) -g1
#x2 #Hx2 * -g2
#H lapply (injective_next … H) -H //
qed-.
-lemma eq_inv_pn: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f1,f2. â\86\91f1 = g1 â\86\92 ⫯f2 = g2 → ⊥.
+lemma eq_inv_pn: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f1,f2. ⫯f1 = g1 â\86\92 â\86\91f2 = g2 → ⊥.
#g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_px … H … H1) -g1
#x2 #Hx2 * -g2
#H elim (discr_next_push … H)
qed-.
-lemma eq_inv_np: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f1,f2. ⫯f1 = g1 â\86\92 â\86\91f2 = g2 → ⊥.
+lemma eq_inv_np: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f1,f2. â\86\91f1 = g1 â\86\92 ⫯f2 = g2 → ⊥.
#g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_nx … H … H1) -g1
#x2 #Hx2 * -g2
#H elim (discr_push_next … H)
qed-.
-lemma eq_inv_gen: â\88\80f1,f2. f1 â\89\97 f2 →
- (â\88\83â\88\83g1,g2. g1 â\89\97 g2 & â\86\91g1 = f1 & â\86\91g2 = f2) ∨
- â\88\83â\88\83g1,g2. g1 â\89\97 g2 & ⫯g1 = f1 & ⫯g2 = f2.
+lemma eq_inv_gen: â\88\80f1,f2. f1 â\89¡ f2 →
+ (â\88\83â\88\83g1,g2. g1 â\89¡ g2 & ⫯g1 = f1 & ⫯g2 = f2) ∨
+ â\88\83â\88\83g1,g2. g1 â\89¡ g2 & â\86\91g1 = f1 & â\86\91g2 = f2.
#f1 elim (pn_split f1) * #g1 #H1 #f2 #Hf
[ elim (eq_inv_px … Hf … H1) -Hf /3 width=5 by or_introl, ex3_2_intro/
| elim (eq_inv_nx … Hf … H1) -Hf /3 width=5 by or_intror, ex3_2_intro/
/3 width=5 by eq_push, eq_next/
qed-.
-theorem eq_canc_sn: â\88\80f2. eq_repl_back (λf. f â\89\97 f2).
+theorem eq_canc_sn: â\88\80f2. eq_repl_back (λf. f â\89¡ f2).
/3 width=3 by eq_trans, eq_sym/ qed-.
-theorem eq_canc_dx: â\88\80f1. eq_repl_fwd (λf. f1 â\89\97 f).
+theorem eq_canc_dx: â\88\80f1. eq_repl_fwd (λf. f1 â\89¡ f).
/3 width=3 by eq_trans, eq_sym/ qed-.