(* *)
(**************************************************************************)
-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 *********************************************************)
-let corec eq_refl: reflexive … eq ≝ ?.
+corec lemma eq_refl: reflexive … eq.
#f cases (pn_split f) *
#g #Hg [ @(eq_push … Hg Hg) | @(eq_next … Hg Hg) ] -Hg //
qed.
-let corec eq_sym: symmetric … eq ≝ ?.
+corec lemma eq_sym: symmetric … eq.
#f1 #f2 * -f1 -f2
#f1 #f2 #g1 #g2 #Hf #H1 #H2
[ @(eq_push … H2 H1) | @(eq_next … H2 H1) ] -g2 -g1 /2 width=1 by/
(* 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/
(* Main properties **********************************************************)
-let corec eq_trans: Transitive … eq ≝ ?.
+corec theorem eq_trans: Transitive … eq.
#f1 #f * -f1 -f
#f1 #f #g1 #g #Hf1 #H1 #H #f2 #Hf2
[ cases (eq_inv_px … Hf2 … H) | cases (eq_inv_nx … Hf2 … H) ] -g
/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-.