source: src/RTLabs/CostInj.ma @ 2418

include "RTLabs/Traces.ma".

(* Check that the RTLabs pc → cost label map is injective for a given RTLabs
   program.
   
   First we check functions individually, then lift to the whole program. *)

definition graph_cost_injectivity : graph statement → Prop ≝
λg. ∀l1,l2,PR1,PR2,cl.
  cost_label_of (lookup_present ?? g l1 PR1) = Some ? cl →
  cost_label_of (lookup_present ?? g l2 PR2) = Some ? cl →
  l1 = l2.

definition function_cost_injectivity ≝
λf. graph_cost_injectivity (f_graph f).

definition program_cost_injectivity : RTLabs_program → Prop ≝
λp. All ? (λx. match \snd x with [ Internal f ⇒ function_cost_injectivity f | _ ⇒ True]) (prog_funct … p).

definition reverse_label_map : graph statement → (option (identifier_map CostTag (identifier LabelTag))) ≝
λg.
  foldi
    statement
    (option (identifier_map CostTag (identifier LabelTag)))
    LabelTag
    (λl,s,m.
      match m with
      [ None ⇒ None ?
      | Some m ⇒
        match cost_label_of s with
        [ Some cl ⇒
          match lookup ?? m cl with
          [ None ⇒ Some ? (add … m cl l)
          | Some _ ⇒ None ?
          ]
        | None ⇒ Some ? m
        ]
      ])
    g
    (Some ? (empty_map …)).


definition check_fun_inj : internal_function → bool ≝
λf.
match reverse_label_map (f_graph f) with
[ None ⇒ false
| Some _ ⇒ true
].

definition domain_of_pm : ∀A. positive_map A → positive_map unit ≝
λA,t. fold A (positive_map unit) (λp,a,b. insert unit p it b) t (pm_leaf unit).

lemma pm_fold_ignore_adding_junk : ∀A. ∀m. ∀f,g:Pos → Pos. ∀s.
  (∀p,q. f p ≠ g q) →
  ∀p. lookup_opt unit (f p) (fold A ? (λx,a,b. insert unit (g x) it b) m s) = lookup_opt unit (f p) s.
#A #m elim m
[ normalize //
| #oa #l #r #IHl #IHr
  #f #g #s #not_g #p
  normalize
  >IHr
  [ >IHl
    [ cases oa
      [ normalize %
      | #a normalize >(lookup_opt_insert_miss ?? (f p)) [ % | @not_g ]
      ]
    | #x #y % #E cases (not_g x (p0 y)) #H @H @E
    ]
  | #x #y % #E cases (not_g x (p1 y)) #H @H @E
  ]
] qed.

lemma pm_fold_ind_gen : ∀A,B,m,f,b.
  ∀pre:Pos→Pos. (∀x,y.pre x = pre y → x = y) → ∀ps. (∀p. lookup_opt ? (pre p) ps = None ?) →
  ∀P:B → positive_map unit → Prop.
  P b ps →
  (∀p,ps,a,b. lookup_opt unit (pre p) ps = None unit → lookup_opt A p m = Some A a → P b ps → P (f (pre p) a b) (insert unit (pre p) it ps)) →
  P (fold A B (λx. f (pre x)) m b) (fold ?? (λp,a,b. insert unit (pre p) it b) m ps).
#A #B #m elim m
[ //
| #oa #l #r #IHl #IHr
  #f #b #pre #PRE #ps #PS #P #emp #step whd in ⊢ (?%%);
  @IHr
  [ #x #y #E lapply (PRE … E) #E' destruct //
  | #p change with ((λx. pre (p1 x)) p) in match (pre (p1 p)); >pm_fold_ignore_adding_junk
    [ cases oa [ @PS | #a >(lookup_opt_insert_miss ?? (pre (p1 p))) [ @PS | % #E lapply (PRE … E) #E' destruct ] ]
    | #p #q % #E lapply (PRE … E) #E' destruct
    ]
  | @IHl
    [ #x #y #E lapply (PRE … E) #E' destruct //
    | #p cases oa [ @PS | #a >(lookup_opt_insert_miss ?? (pre (p0 p))) [ @PS | % #E lapply (PRE … E) #E' destruct ] ]
    | cases oa in step ⊢ %; [ #_ @emp | #a #step normalize @step [ @PS | % | @emp ] ]
    | #p #ps' #a #b' @step
    ]
  | #p #ps' #a #b' @step
  ]
] qed.

lemma pm_fold_ext : ∀A,B,m,f,b.
  fold A B f m b = fold A B (λx:Pos. f x) m b.
#A #B #m elim m /4/
qed.

lemma pm_fold_ind : ∀A,B,f,m,b. ∀P:B → positive_map unit → Prop.
  P b (pm_leaf unit) →
  (∀p,ps,a,b. lookup_opt unit p ps = None unit → lookup_opt A p m = Some A a → P b ps → P (f p a b) (insert unit p it ps)) →
  P (fold A B f m b) (domain_of_pm A m).
#A #B #f #m #b #P #emp #step
>pm_fold_ext
whd in ⊢ (??%);
@(pm_fold_ind_gen A B m f b (λx.x) ? (pm_leaf unit) ???)
[ //
| //
| @emp
| @step
] qed.

lemma pm_fold_eq : ∀A,B,b,f.
  (∀p,k:Pos. ∀a,s1,s2. lookup_opt B p s1 = lookup_opt B p s2 → lookup_opt B p (f k a s1) = lookup_opt B p (f k a s2)) →
  ∀p,s1,s2.
  lookup_opt B p s1 = lookup_opt B p s2 →
  lookup_opt B p (fold A (positive_map B) f b s1) = lookup_opt B p (fold A (positive_map B) f b s2).
#A #B #b elim b
[ #f #H #p #s1 #s2 #H @H
| #oa #l #r #IHl #IHr #f #H #p #s1 #s2 #H'
  whd in match (fold ???? s1);
  whd in match (fold ???? s2);
  @IHr [ #q #k #a #s1' #s2' #H'' @H @H'' ]
  @IHl [ #q #k #a #s1' #s2' #H'' @H @H'' ]
  cases oa [ @H' | #a @H @H' ]
] qed.



lemma pm_fold_ignore_prefix : ∀A. ∀m. ∀pre:Pos → Pos. (∀x,y. pre x = pre y → x = y) →
  ∀p. ∀pre'.
      lookup_opt unit (pre p) (fold A ? (λx,a,b. insert unit (pre (pre' x)) it b) m (pm_leaf ?)) =
      lookup_opt unit p (fold A ? (λx,a,b. insert unit (pre' x) it b) m (pm_leaf ?)).
#A #m #pre #PRE
cut (∀p. lookup_opt unit (pre p) (pm_leaf unit) = lookup_opt unit p (pm_leaf unit)) [ // ]
generalize in match (pm_leaf unit) in ⊢ ((? → ??%?) → ? → ? → ??%?);
generalize in match (pm_leaf unit);
elim m
[ #s1 #s2 #S #p #pre' @S 
| #oa #l #r #IHl #IHr
  #s1 #s2 #S #p #pre'
  whd in ⊢ (??(???%)(???%));
  @(IHr ???? (λx. pre' (p1 x)))
  #p' @IHl
  #p'' cases oa
  [ @S
  | #a cases (decidable_eq_pos p'' (pre' one))
    [ #E destruct
      >(lookup_opt_insert_hit ?? (pre (pre' one)))
      >(lookup_opt_insert_hit ?? (pre' one))
      %
    | #NE >(lookup_opt_insert_miss ??? (pre (pre' one)))
      [ >(lookup_opt_insert_miss ??? (pre' one)) //
      | % #E @(absurd … (PRE … E) NE)
      ]
    ]
  ]
] qed.

lemma domain_of_pm_present : ∀A,m,p.
  lookup_opt A p m ≠ None ? ↔ lookup_opt unit p (domain_of_pm A m) ≠ None ?.

#A #m whd in match (domain_of_pm ??);
elim m
[ #p normalize /3/
| #oa #l #r #IHl #IHr
  whd in match (fold ???? (pm_leaf unit));
  *
  [ change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?)));
    >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ]
    change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?)));
    >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ]
    cases oa
    [ normalize /3/
    | #a change with (insert unit one ??) in ⊢ (??(?(??(???%)?)));
      >(lookup_opt_insert_hit ?? one) normalize
      % #_ % #E destruct
    ]
  | #p >(pm_fold_eq ??????? (pm_leaf unit))
    [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ]
      @IHr
    | >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ]
      cases oa
      [ %
      | #a >(lookup_opt_insert_miss ?? (p1 p)) [2: % #E destruct ]
        %
      ]
    | #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p1 y))
      [ #E destruct
        >(lookup_opt_insert_hit ?? (p1 y))
        >(lookup_opt_insert_hit ?? (p1 y))
        %
      | #NE >(lookup_opt_insert_miss ?? x … NE)
        >(lookup_opt_insert_miss ?? x … NE)
        @S
      ]
    ]  
  | #p
    >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ]
    >(pm_fold_eq ??????? (pm_leaf unit))
    [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ]
      @IHl
    | cases oa
      [ %
      | #a >(lookup_opt_insert_miss ?? (p0 p)) [2: % #E destruct ]
        %
      ]
    | #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p0 y))
      [ #E destruct
        >(lookup_opt_insert_hit ?? (p0 y))
        >(lookup_opt_insert_hit ?? (p0 y))
        %
      | #NE >(lookup_opt_insert_miss ?? x … NE)
        >(lookup_opt_insert_miss ?? x … NE)
        @S
      ]
    ]
  ]
] qed.


(* Returns the domain of a map as the canonical set (one made only from the
   empty set and addition. *)
definition domain_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
λtag,A,m. an_id_map tag unit (domain_of_pm A (match m with [ an_id_map m ⇒ m ])).
lemma domain_of_map_present : ∀tag,A,m,id.
  present tag A m id ↔ present tag unit (domain_of_map … m) id.
#tag #A * #m * #p @domain_of_pm_present
qed.

lemma foldi_ind : ∀A,B,tag,f,m,b. ∀P:B → identifier_set tag → Prop.
  P b (empty_set …) →
  (∀k,ks,a,b. ¬present ?? ks k → lookup ?? m k = Some ? a → P b ks → P (f k a b) (add_set tag ks k)) →
  P (foldi A B tag f m b) (domain_of_map … m).
#A #B #tag #f * #m #b #P #P0 #STEP
whd in match (foldi ??????); change with (an_id_map ?? (domain_of_pm A m)) in match (domain_of_map ???);
@pm_fold_ind
[ @P0
| #p #ps #a #b0 #FR #L #pre @(STEP (an_identifier tag p) (an_id_map tag unit ps))
  [ normalize >FR /3/
  | @L
  | @pre
  ]
] qed.

lemma foldi_ind' : ∀A,B,tag,f,m,b,b'. ∀P:B → identifier_set tag → Prop.
  P b (empty_set …) →
  (∀k,ks,a,b. ¬present ?? ks k → lookup ?? m k = Some ? a → P b ks → P (f k a b) (add_set tag ks k)) →
  foldi A B tag f m b = b' →
  P b' (domain_of_map … m).
#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11  destruct @foldi_ind /2/
qed.

lemma reverse_label_map_ok : ∀g,r.
  reverse_label_map g = r →
  match r with
  [ None ⇒ ¬graph_cost_injectivity g
  | Some m ⇒ graph_cost_injectivity g
  ].
#g #r #F change with (foldi ??????) in F:(??%?);
lapply (foldi_ind' ??????? (λm,ls.
  match m with
  [ None ⇒ ¬(graph_cost_injectivity g)
  | Some m ⇒ ∀l,cl. (present ?? ls l ∧ ∃PR. cost_label_of (lookup_present ?? g l PR) = Some ? cl) ↔ lookup ?? m cl = Some ? l
  ]) ?? F)
[ #l #ls #s *
  [ #FR #L #H whd in H ⊢ %; @H
  | #m #FR #L #H whd in H ⊢ (match % with [_⇒?|_⇒?]);
    lapply (refl ? (cost_label_of s)) cases (cost_label_of s) in ⊢ (???% → %);
    [ #NCS whd #l' #cl cases (H l' cl) #H1 #H2 %
      [ * #H3 * #PR' #H4 cases (present_add_cases ?????? H3)
        [ #E destruct @⊥ >(lookup_present_eq ????? L ?) in H4; >NCS #E destruct
        | * #_ #PR'' @H1 /3/
        ]
      | #Lcl cases (H2 Lcl) #PR'' * #PR''' #CS % /2/
      ]
    | #cl #CL whd in  ⊢ (match % with [_⇒?|_⇒?]);
      lapply (refl ? (lookup ?? m cl)) cases (lookup ?? m cl) in ⊢ (???% → %);
      [ #Lcl whd #l' #cl' cases (H l' cl') #H1 #H2 %
        [ * #H3 * #PRg' #H4 cases (present_add_cases ?????? H3)
          [ #E destruct >(lookup_present_eq ????? L ?) in H4; >CL #E destruct
            @lookup_add_hit
          | * #NE #PR'' lapply (H1 ?) [/3/] #Lcl' >lookup_add_miss [ // | % #E destruct >Lcl in Lcl'; #E destruct ]
          ]
        | #Lcl' cases (lookup_add_cases ??????? Lcl')
          [ * #E1 #E2 destruct % [ @present_add_hit | %{(lookup_is_present … L)} >(lookup_present_eq ????? L ?) assumption ]
          | #Lcl'' cases (H2 Lcl'') /3/
          ]
        ]
      | #l' #L' whd % #GCI whd in GCI;
        cases (H l' cl) #H1 #H2 cases (H2 L') #PR' * #PRg' #CS'
        lapply (GCI l l' (lookup_is_present … L) PRg' cl ??)
        [ assumption
        | >(lookup_present_eq ????? L ?) assumption
        | #E destruct /2/
        ]
      ]
    ]
  ]
| whd #l #cl %
  [ * * #H cases (H (refl ??))
  | #E normalize in E; destruct
  ]
| cases r
  [ //
  | #m whd in ⊢ (% → %); #H
    #l1 #l2 #PR1 #PR2 #cl #CL1 #CL2
    cases (H l1 cl) #H1 #_ lapply (H1 ?) [ % [ @(proj1 … (domain_of_map_present … )) // | %{PR1} @CL1 ] ]
    cases (H l2 cl) #H2 #_ lapply (H2 ?) [ % [ @(proj1 … (domain_of_map_present … )) // | %{PR2} @CL2 ] ]
    #E >E #E' destruct %
  ]
] qed.

lemma check_fun_inj_ok : ∀f. bool_to_Prop (check_fun_inj f) ↔ function_cost_injectivity f.
#f %
[ whd in ⊢ (?% → ?);
  lapply (reverse_label_map_ok (f_graph f))
  cases (reverse_label_map ?)
  [ #_ *
  | #m #H #_ @(H (Some ? m)) %
  ]
| lapply (reverse_label_map_ok (f_graph f))
  whd in ⊢ (? → ? → ?%);
  cases (reverse_label_map ?)
  [ #H #INJ @(absurd … INJ (H (None ?) (refl ??)))
  | //
  ]
] qed.

definition check_program_cost_injectivity : RTLabs_program → bool ≝
λp. all ? (λx. match \snd x with [ Internal f ⇒ check_fun_inj f | _ ⇒ true ]) (prog_funct … p).

theorem check_project_cost_injectivity_ok : ∀p.
  bool_to_Prop (check_program_cost_injectivity p) ↔ program_cost_injectivity p.
#p %
[ #H whd in H:(?%) ⊢ %;
  @(All_mp ????? (proj1 … (all_All …) H))
  * #_ * // #f @(proj1 … (check_fun_inj_ok f))
| whd in ⊢ (% → ?%);
  #H
  @(proj2 … (all_All …))
  @(All_mp … H)
  * #_ * // #f
  @(proj2 … (check_fun_inj_ok f))
] qed.