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/isidentity_1.ma".
16 include "ground_2/relocation/rtmap_tls.ma".
18 (* RELOCATION MAP ***********************************************************)
20 coinductive isid: predicate rtmap ≝
21 | isid_push: ∀f,g. isid f → ↑f = g → isid g
24 interpretation "test for identity (rtmap)"
25 'IsIdentity f = (isid f).
27 (* Basic inversion lemmas ***************************************************)
29 lemma isid_inv_gen: ∀g. 𝐈⦃g⦄ → ∃∃f. 𝐈⦃f⦄ & ↑f = g.
31 #f #g #Hf * /2 width=3 by ex2_intro/
34 (* Advanced inversion lemmas ************************************************)
36 lemma isid_inv_push: ∀g. 𝐈⦃g⦄ → ∀f. ↑f = g → 𝐈⦃f⦄.
37 #g #H elim (isid_inv_gen … H) -H
38 #f #Hf * -g #g #H >(injective_push … H) -H //
41 lemma isid_inv_next: ∀g. 𝐈⦃g⦄ → ∀f. ⫯f = g → ⊥.
42 #g #H elim (isid_inv_gen … H) -H
43 #f #Hf * -g #g #H elim (discr_next_push … H)
46 let corec isid_inv_eq_repl: ∀f1,f2. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → f1 ≗ f2 ≝ ?.
48 cases (isid_inv_gen … H1) -H1
49 cases (isid_inv_gen … H2) -H2
50 /3 width=5 by eq_push/
53 (* Basic properties *********************************************************)
55 let corec isid_eq_repl_back: eq_repl_back … isid ≝ ?.
56 #f1 #H cases (isid_inv_gen … H) -H
57 #g1 #Hg1 #H1 #f2 #Hf cases (eq_inv_px … Hf … H1) -f1
58 /3 width=3 by isid_push/
61 lemma isid_eq_repl_fwd: eq_repl_fwd … isid.
62 /3 width=3 by isid_eq_repl_back, eq_repl_sym/ qed-.
64 (* Alternative definition ***************************************************)
66 let corec eq_push_isid: ∀f. ↑f ≗ f → 𝐈⦃f⦄ ≝ ?.
67 #f #H cases (eq_inv_px … H) -H /4 width=3 by isid_push, eq_trans/
70 let corec eq_push_inv_isid: ∀f. 𝐈⦃f⦄ → ↑f ≗ f ≝ ?.
72 #f #g #Hf #Hg @(eq_push … Hg) [2: @eq_push_inv_isid // | skip ]