include "common/Identifiers.ma".
include "utilities/lists.ma".
include alias "arithmetics/nat.ma".

definition labelled_obj ≝ λtag,A.(option (identifier tag)) × A.

definition instruction_matches_identifier ≝
  λtag,A.
  λy: identifier tag.
  λx: labelled_obj tag A.
    match \fst x with
    [ None ⇒ false
    | Some x ⇒ eq_identifier ? x y
    ].

let rec does_not_occur tag A (id : identifier tag) (l : list (labelled_obj tag A))
  on l : bool ≝ match l with
  [ nil ⇒ true
  | cons x l ⇒ ¬instruction_matches_identifier … id x ∧ does_not_occur tag A id l
  ].

lemma does_not_occur_append : ∀tag,A,id,l1,l2.
  does_not_occur tag A id (l1@l2) =
    (does_not_occur tag A id l1 ∧ does_not_occur tag A id l2).
#tag #A #id #l1 elim l1
[ // ]
#hd #tl #IH #l2 whd in match (does_not_occur ????) in ⊢ (??%%);
>IH elim (¬instruction_matches_identifier ?? id hd) %
qed.

lemma does_not_occur_None:
 ∀tag,A,id,i,list_instr.
  does_not_occur tag A id (list_instr@[〈None …,i〉]) =
  does_not_occur tag A id list_instr.
 #tag #A #id #i #list_instr
 >does_not_occur_append @commutative_andb
qed.

lemma does_not_occur_Some:
 ∀tag,A,id,id',i,list_instr.
  eq_identifier ? id' id = false →
   does_not_occur tag A id (list_instr@[〈Some ? id',i〉]) =
    does_not_occur … id list_instr.
 #tag #A #id #id' #i #list_instr #eq_id_false
 >does_not_occur_append >commutative_andb
 whd in match (does_not_occur ??? [?]);
 change with (eq_identifier ???) in match (instruction_matches_identifier ????);
 >eq_id_false
 %
qed.

lemma does_not_occur_absurd:
 ∀tag,A,id,i,list_instr.
  does_not_occur tag A id (list_instr@[〈Some ? id,i〉]) = false.
 #tag #A #id #i #list_instr
 >does_not_occur_append >commutative_andb
 whd in match (does_not_occur ??? [?]);
 change with (eq_identifier ???) in match (instruction_matches_identifier ????);
 >eq_identifier_refl %
qed.

let rec occurs_exactly_once tag A (id : identifier tag) (l : list (labelled_obj tag A))
  on l : bool ≝ match l with
  [ nil ⇒ false
  | cons x l ⇒
    if instruction_matches_identifier … id x then
      does_not_occur … id l
    else
      occurs_exactly_once … id l
  ].
  
lemma occurs_exactly_once_append : ∀tag,A,id,l1,l2.
  occurs_exactly_once tag A id (l1@l2) =
    ((occurs_exactly_once … id l1 ∧ does_not_occur … id l2) ∨
     (does_not_occur … id l1 ∧ occurs_exactly_once … id l2)).
#tag #A #id #l1 elim l1
[ // ]
#hd #tl #IH #l2
whd in match (occurs_exactly_once ????) in ⊢ (??%(?%%));
whd in match (does_not_occur ????) in ⊢ (???(?%%));
>does_not_occur_append
>IH
elim (instruction_matches_identifier … id hd) normalize nodelta
>commutative_orb %
qed.

lemma occurs_exactly_once_None:
 ∀tag,A,id,i,list_instr.
  occurs_exactly_once tag A id (list_instr@[〈None …,i〉]) =
  occurs_exactly_once … id list_instr.
 #tag #A #id #i #list_instr
 >occurs_exactly_once_append normalize
 elim (occurs_exactly_once ?? id list_instr) [%]
 elim (does_not_occur ?? id list_instr) %
qed.

lemma occurs_exactly_once_Some:
 ∀tag,A,id,id',i,prefix.
  occurs_exactly_once tag A id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once … id prefix.
 #tag #A #id #id' #i #prefix
 >occurs_exactly_once_append #H elim(orb_Prop_true ?? H) -H
 #H elim (andb_Prop_true ?? H) -H
 [ whd in match (does_not_occur ????); | whd in match (occurs_exactly_once ????);]
  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
  elim (eq_identifier ???) normalize #H * //
qed. 

lemma occurs_exactly_once_Some_stronger:
  ∀tag,A,id,id',i,prefix.
    occurs_exactly_once tag A id (prefix@[〈Some ? id',i〉]) → 
    (eq_identifier ? id' id ∧ does_not_occur … id prefix) ∨
    (¬eq_identifier ? id' id ∧ occurs_exactly_once … id prefix).
 #tag #A #id #id' #i #prefix
 >occurs_exactly_once_append
 #H elim(orb_Prop_true ?? H) -H
 #H elim (andb_Prop_true ?? H) -H
 [ whd in match (does_not_occur ????); | whd in match (occurs_exactly_once ????);]
  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
  elim (eq_identifier ???) #H * >H //
qed.

lemma occurs_exactly_once_Some_eq :
  ∀tag,A,id,id',i,prefix.
    occurs_exactly_once tag A id (prefix@[〈Some ? id',i〉]) =
      if eq_identifier ? id' id then
        does_not_occur … id prefix
      else
        occurs_exactly_once … id prefix.
 #tag #A #id #id' #i #prefix
 >occurs_exactly_once_append
 normalize in match (does_not_occur ????) in ⊢ (??(?%?)?);
 normalize in match (occurs_exactly_once ????) in ⊢ (??(??%)?);
 change with (eq_identifier ???) in match (match ? with [an_identifier _ ⇒ ?]) in ⊢ (??(?%%)?);
 elim (eq_identifier ???)
 elim (does_not_occur … id prefix)
 elim (occurs_exactly_once … id prefix) %
qed.

let rec index_of_internal A (test : A → bool) (l : list A) acc on l : ℕ ≝
  match l with
  [ nil ⇒ ?
  | cons x tl ⇒ if test x then acc else index_of_internal A test tl (S acc)
  ].
cases not_implemented
qed.

definition index_of ≝ λA,test,l.index_of_internal A test l 0.

lemma index_of_internal_None: ∀tag,A,i,id,instr_list,n.
 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
   index_of_internal ? (instruction_matches_identifier tag A id) instr_list n =
   index_of_internal ? (instruction_matches_identifier tag A id) (instr_list@[〈None …,i〉]) n.
 #tag #A #i #id #instr_list >occurs_exactly_once_None
  elim instr_list
  [ #n *
  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
    cases (instruction_matches_identifier ????) normalize nodelta [ #_ % ]
    #H @(IH ? H)
  ]
qed.

lemma index_of_internal_Some_miss: ∀tag,A,i,id,id'.
 eq_identifier ? id' id = false →
 ∀instr_list,n.
 occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
  index_of_internal ? (instruction_matches_identifier tag A id) instr_list n =
   index_of_internal ? (instruction_matches_identifier ?? id) (instr_list@[〈Some ? id',i〉]) n.
 #tag #A #i #id #id' #EQ #instr_list #n
 >occurs_exactly_once_Some_eq >EQ normalize nodelta
 generalize in match n; -n elim instr_list
  [ #n *
  | #hd #tl #IH #n whd in ⊢ (?% → ??%%);
    cases (instruction_matches_identifier ?? id hd)
    normalize nodelta
    [ // | #K @IH //]]
qed.

lemma index_of_internal_Some_hit: ∀tag,A,i,id.
 ∀instr_list,n.
  occurs_exactly_once tag A id (instr_list@[〈Some ? id,i〉]) →
   index_of_internal ? (instruction_matches_identifier tag A id) (instr_list@[〈Some ? id,i〉]) n
  = |instr_list| + n.
 #tag #A #i #id #instr_list #n
  >occurs_exactly_once_Some_eq >eq_identifier_refl normalize nodelta lapply n -n 
  elim instr_list
  [ #n #_ whd in ⊢ (??%%); change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %
  | #hd #tl #IH #n whd in ⊢ (?% → ??%%);
    cases (instruction_matches_identifier ?? id hd)
    normalize nodelta
    [ * | #H >plus_n_Sm <(IH (S n)) //]]
qed.

definition index_of_label : ∀tag,A.identifier tag →
  list (labelled_obj tag A) → ℕ ≝
  λtag,A,l.index_of ? (instruction_matches_identifier ?? l).
  
lemma index_of_label_from_internal : ∀tag,A,id,instrs,n.
  occurs_exactly_once tag A id instrs →
    index_of_internal ? (instruction_matches_identifier ?? id) instrs n =
      n + index_of_label ?? id instrs.
#tag #A #id #instrs elim instrs
[ #n *
| **[2: #lbl] #s #tl #IH #n
  whd in match (occurs_exactly_once ????);
  whd in match (index_of_label ????);
  whd in match (index_of_internal ????);
  [ change with (eq_identifier ???) in match (instruction_matches_identifier ????);
    @eq_identifier_elim #Heq normalize nodelta
    [ #_ @plus_n_O ] ]
  #Htl >(IH ? Htl) >(IH ? Htl)
  [ generalize in match (index_of_label ?? id tl);
  | generalize in match (index_of_label ?? id tl);
  ] /2 by plus_minus_m_m/
]
qed.
  
lemma index_of_label_nth_opt : ∀tag,A,id,instrs.
  occurs_exactly_once tag A id instrs →
    ∃s.nth_opt ? (index_of_label tag A id instrs) instrs = Some ? 〈Some ? id, s〉.
#tag #A #id #instrs elim instrs
[ *
| * * [2: #lbl] #s #tl #IH
  whd in match (occurs_exactly_once ????);
  whd in match (index_of_label ????);
  [ change with (eq_identifier ???) in match (instruction_matches_identifier ????);
    @eq_identifier_elim #Heq normalize nodelta
    [ #_ %{s} >Heq % ] ]
  #occ_once_tl
  >(index_of_label_from_internal … occ_once_tl)
  whd in match (nth_opt ???);
  @IH assumption
]
qed.

lemma does_not_occur_All : ∀tag,A,id,instrs.does_not_occur tag A id instrs →
  All ? (λls.¬(bool_to_Prop (instruction_matches_identifier tag A id ls))) instrs.
#tag #A #id #instrs elim instrs
[ * %
| * * [2: #lbl] #s #tl #IH
  whd in match (does_not_occur ????);
  #H % 
  [1: lapply H -H 
    change with (eq_identifier ???) in match (instruction_matches_identifier ????);
    @eq_identifier_elim #Heq normalize nodelta [1,3:* |*: #_ % *]
  |3: % *
  |*: @IH
    [elim (¬(instruction_matches_identifier ????)) in H; normalize nodelta [ #H | *]]
    assumption
  ]
]
qed.

lemma nth_opt_index_of_label : ∀tag,A,id,instrs,n,s.
  occurs_exactly_once tag A id instrs →
    nth_opt ? n instrs = Some ? 〈Some ? id, s〉 → index_of_label ?? id instrs = n.
#tag #A #id #instrs elim instrs
[ #n #s *
| * * [2: #lbl] #s #tl #IH #n #s'
  whd in match (occurs_exactly_once ????);
  whd in match (index_of_label ????);
  [ change with (eq_identifier ???) in match (instruction_matches_identifier ????);
    @eq_identifier_elim #Heq normalize nodelta
    [ #no_id_in_tl cases n [#_ %] -n #n whd in match (nth_opt ???); #nth_opt_n
    lapply (All_nth ???? (does_not_occur_All … no_id_in_tl) ? nth_opt_n)
    change with (eq_identifier ???) in match (instruction_matches_identifier ????);
    >eq_identifier_refl * #H elim (H I) ] ]
  #occ_once_tl
  >(index_of_label_from_internal … occ_once_tl)
  cases n [2,4: -n #n] whd in match (nth_opt ???);
  [3,4:  #ABS destruct(ABS) elim Heq #ABS' elim (ABS' ?) %
  |*: #H >(IH … H) [1,3: %] assumption
  ]
]
qed.