matita/matita/contribs/lambdadelta/ground/relocation/nstream_coafter.ma

   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 N-STREAM ******************************************************)
  19
  20 rec definition fun0 (n1:nat) on n1: rtmap → nat.
  21 * * [ | #n2 #f2 @0 ]
  22 #f2 cases n1 -n1 [ @0 ]
  23 #n1 @(↑(fun0 n1 f2))
  24 defined.
  25
  26 rec definition fun2 (n1:nat) on n1: rtmap → rtmap.
  27 * * [ | #n2 #f2 @(n2⨮f2) ]
  28 #f2 cases n1 -n1 [ @f2 ]
  29 #n1 @(fun2 n1 f2)
  30 defined.
  31
  32 rec definition fun1 (n1:nat) (f1:rtmap) on n1: rtmap → rtmap.
  33 * * [ | #n2 #f2 @(n1⨮f1) ]
  34 #f2 cases n1 -n1 [ @f1 ]
  35 #n1 @(fun1 n1 f1 f2)
  36 defined.
  37
  38 corec definition cocompose: rtmap → rtmap → rtmap.
  39 #f2 * #n1 #f1 @(seq … (fun0 n1 f2)) @(cocompose (fun2 n1 f2) (fun1 n1 f1 f2))
  40 defined.
  41
  42 interpretation "functional co-composition (nstream)"
  43    'CoCompose f1 f2 = (cocompose f1 f2).
  44
  45 (* Basic properties on funs *************************************************)
  46
  47 (* Note: we need theese since matita blocks recursive δ when ι is blocked *)
  48 lemma fun0_xn: ∀f2,n1. 0 = fun0 n1 (↑f2).
  49 * #n2 #f2 * //
  50 qed.
  51
  52 lemma fun2_xn: ∀f2,n1. f2 = fun2 n1 (↑f2).
  53 * #n2 #f2 * //
  54 qed.
  55
  56 lemma fun1_xxn: ∀f2,f1,n1. fun1 n1 f1 (↑f2) = n1⨮f1.
  57 * #n2 #f2 #f1 * //
  58 qed.
  59
  60 (* Basic properies on cocompose *********************************************)
  61
  62 lemma cocompose_rew: ∀f2,f1,n1. (fun0 n1 f2)⨮(fun2 n1 f2)~∘(fun1 n1 f1 f2) = f2 ~∘ (n1⨮f1).
  63 #f2 #f1 #n1 <(stream_rew … (f2~∘(n1⨮f1))) normalize //
  64 qed.
  65
  66 (* Basic inversion lemmas on compose ****************************************)
  67
  68 lemma cocompose_inv_ppx: ∀f2,f1,f,x. (⫯f2) ~∘ (⫯f1) = x⨮f →
  69                          0 = x ∧ f2 ~∘ f1 = f.
  70 #f2 #f1 #f #x
  71 <cocompose_rew #H destruct
  72 normalize /2 width=1 by conj/
  73 qed-.
  74
  75 lemma cocompose_inv_pnx: ∀f2,f1,f,n1,x. (⫯f2) ~∘ (↑n1⨮f1) = x⨮f →
  76                          ∃∃n. ↑n = x & f2 ~∘ (n1⨮f1) = n⨮f.
  77 #f2 #f1 #f #n1 #x
  78 <cocompose_rew #H destruct
  79 @(ex2_intro … (fun0 n1 f2)) // <cocompose_rew
  80 /3 width=1 by eq_f2/
  81 qed-.
  82
  83 lemma cocompose_inv_nxx: ∀f2,f1,f,n1,x. (↑f2) ~∘ (n1⨮f1) = x⨮f →
  84                          0 = x ∧ f2 ~∘ (n1⨮f1) = f.
  85 #f2 #f1 #f #n1 #x
  86 <cocompose_rew #H destruct
  87 /2 width=1 by conj/
  88 qed-.
  89
  90 (* Specific properties on coafter *******************************************)
  91
  92 corec lemma coafter_total_aux: ∀f2,f1,f. f2 ~∘ f1 = f → f2 ~⊚ f1 ≘ f.
  93 * #n2 #f2 * #n1 #f1 * #n #f cases n2 -n2
  94 [ cases n1 -n1
  95   [ #H cases (cocompose_inv_ppx … H) -H /3 width=7 by coafter_refl, eq_f2/
  96   | #n1 #H cases (cocompose_inv_pnx … H) -H /3 width=7 by coafter_push/
  97   ]
  98 | #n2 >next_rew #H cases (cocompose_inv_nxx … H) -H /3 width=5 by coafter_next/
  99 ]
 100 qed-.
 101
 102 theorem coafter_total: ∀f2,f1. f2 ~⊚ f1 ≘ f2 ~∘ f1.
 103 /2 width=1 by coafter_total_aux/ qed.