matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_coafter.etc

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "ground/notation/functions/cocompose_2.ma".
  16 include "ground/relocation/rtmap_coafter.ma".
  17
  18 (* RELOCATION P-STREAM ******************************************************)
  19
  20 rec definition fun0 (p1:pnat) on p1: gr_map → pnat.
  21 * * [ | #p2 #f2 @(𝟏) ]
  22 #f2 cases p1 -p1 [ @(𝟏) ]
  23 #p1 @(↑(fun0 p1 f2))
  24 defined.
  25
  26 rec definition fun2 (p1:pnat) on p1: gr_map → gr_map.
  27 * * [ | #p2 #f2 @(p2⨮f2) ]
  28 #f2 cases p1 -p1 [ @f2 ]
  29 #p1 @(fun2 p1 f2)
  30 defined.
  31
  32 rec definition fun1 (p1:pnat) (f1:gr_map) on p1: gr_map → gr_map.
  33 * * [ | #p2 #f2 @(p1⨮f1) ]
  34 #f2 cases p1 -p1 [ @f1 ]
  35 #p1 @(fun1 p1 f1 f2)
  36 defined.
  37
  38 corec definition cocompose: gr_map → gr_map → gr_map.
  39 #f2 * #p1 #f1
  40 @(stream_cons … (fun0 p1 f2)) @(cocompose (fun2 p1 f2) (fun1 p1 f1 f2))
  41 defined.
  42
  43 interpretation "functional co-composition (nstream)"
  44    'CoCompose f1 f2 = (cocompose f1 f2).
  45
  46 (* Basic properties on funs *************************************************)
  47
  48 (* Note: we need theese since matita blocks recursive δ when ι is blocked *)
  49 lemma fun0_xn: ∀f2,p1. 𝟏 = fun0 p1 (↑f2).
  50 * #p2 #f2 * //
  51 qed.
  52
  53 lemma fun2_xn: ∀f2,p1. f2 = fun2 p1 (↑f2).
  54 * #p2 #f2 * //
  55 qed.
  56
  57 lemma fun1_xxn: ∀f2,f1,p1. fun1 p1 f1 (↑f2) = p1⨮f1.
  58 * #p2 #f2 #f1 * //
  59 qed.
  60
  61 (* Basic properties on cocompose *********************************************)
  62
  63 lemma cocompose_rew: ∀f2,f1,p1. (fun0 p1 f2)⨮(fun2 p1 f2)~∘(fun1 p1 f1 f2) = f2 ~∘ (p1⨮f1).
  64 #f2 #f1 #p1 <(stream_rew … (f2~∘(p1⨮f1))) normalize //
  65 qed.
  66
  67 (* Basic inversion lemmas on compose ****************************************)
  68
  69 lemma cocompose_inv_ppx: ∀f2,f1,f,x. (⫯f2) ~∘ (⫯f1) = x⨮f →
  70                          ∧∧ 𝟏 = x & f2 ~∘ f1 = f.
  71 #f2 #f1 #f #x
  72 <cocompose_rew #H destruct
  73 normalize /2 width=1 by conj/
  74 qed-.
  75
  76 lemma cocompose_inv_pnx: ∀f2,f1,f,p1,x. (⫯f2) ~∘ (↑p1⨮f1) = x⨮f →
  77                          ∃∃p. ↑p = x & f2 ~∘ (p1⨮f1) = p⨮f.
  78 #f2 #f1 #f #p1 #x
  79 <cocompose_rew #H destruct
  80 @(ex2_intro … (fun0 p1 f2)) // <cocompose_rew
  81 /3 width=1 by eq_f2/
  82 qed-.
  83
  84 lemma cocompose_inv_nxx: ∀f2,f1,f,p1,x. (↑f2) ~∘ (p1⨮f1) = x⨮f →
  85                          ∧∧ 𝟏 = x & f2 ~∘ (p1⨮f1) = f.
  86 #f2 #f1 #f #p1 #x
  87 <cocompose_rew #H destruct
  88 /2 width=1 by conj/
  89 qed-.
  90
  91 (* Properties on coafter (specific) *******************************************)
  92
  93 corec lemma coafter_total_aux: ∀f2,f1,f. f2 ~∘ f1 = f → f2 ~⊚ f1 ≘ f.
  94 * #p2 #f2 * #p1 #f1 * #p #f cases p2 -p2
  95 [ cases p1 -p1
  96   [ #H cases (cocompose_inv_ppx … H) -H /3 width=7 by gr_coafter_refl, eq_f2/
  97   | #p1 #H cases (cocompose_inv_pnx … H) -H /3 width=7 by gr_coafter_push/
  98   ]
  99 | #p2 >gr_next_unfold #H cases (cocompose_inv_nxx … H) -H /3 width=5 by gr_coafter_next/
 100 ]
 101 qed-.
 102
 103 theorem coafter_total: ∀f2,f1. f2 ~⊚ f1 ≘ f2 ~∘ f1.
 104 /2 width=1 by coafter_total_aux/ qed.