include "RTLabs/CostSpec.ma".
include "basics/lists/listb.ma".

(* We aim to extract a loop without a cost label to contradict the reappearance
   of a pc within a trace_any_label.  This data structure represents the tail
   of a loop purely in terms of the RTLabs function body graph. *)

inductive bad_label_list (g:graph statement) (head:label) : label → Prop ≝
| gl_end : bad_label_list g head head
| gl_step : ∀l1,l2,H.
    l2 ∈ successors (lookup_present … g l1 H) →
    ¬ is_cost_label (lookup_present … g l1 H) →
    bad_label_list g head l2 →
    bad_label_list g head l1.

(* Some inversion lemmas on the bounds.

   For the first step just get a bound after the step; we don't care what it is,
   just that it exists. *)
   
lemma bound_step1 : ∀g,l1,n.
  bound_on_instrs_to_cost g l1 n →
  ∀l2,H. Exists ? (λl.l = l2) (successors (lookup_present … g l1 H)) →
  ∃m. bound_on_instrs_to_cost' g l2 m.
#g #l1X #nX * #l #n #H #EX #l2 #H' #EX' %{n} @EX @EX'
qed.

lemma bound_zero1 : ∀g,l.
  ¬ bound_on_instrs_to_cost g l 0.
#g #l % #B lapply (refl ? O) cases B in ⊢ (???% → ?);
#l' #n #H #_ whd in ⊢ (???% → ?); #E destruct
qed.

lemma bound_zero : ∀g,l.
  bound_on_instrs_to_cost' g l 0 →
  ∃H. bool_to_Prop (is_cost_label (lookup_present … g l H)).
#g #l #B
@(match B return λl,n,B. n = O → ∃H. bool_to_Prop (is_cost_label (lookup_present … g l H)) with
  [ boitc_here l n H CS ⇒ ?
  | boitc_later _ _ _ _ B' ⇒ ?
  ] (refl ? O))
[ #E >E %{H} @CS
| #E >E in B'; #B' @⊥ @(absurd … B' (bound_zero1 …))
] qed.

lemma bound_step : ∀g,l,n.
  bound_on_instrs_to_cost' g l (S n) →
  ∃H. (bool_to_Prop (is_cost_label (lookup_present … g l H)) ∨
       (let stmt ≝ lookup_present … g l H in
        ∀l'. Exists label (λl0. l0 = l') (successors stmt) →
             bound_on_instrs_to_cost' g l' n)).
#g #lX #n #B lapply (refl ? (S n)) cases B in ⊢ (???% → %);
[ #l #n #H #CS #E %{H} %1 @CS
| #l #m #H #CS *
  #l' #n' #H' #EX #E destruct %{H'} %2
  #l'' #EX' @EX @EX'
] qed.

lemma bad_label_list_no_cost : ∀g,l1,l2.
  bad_label_list g l1 l2 →
  ∀H1. ¬ is_cost_label (lookup_present … g l1 H1) →
  ∃H2. bool_to_Prop (¬ is_cost_label (lookup_present … g l2 H2)).
#g #l1 #l2 * /2/
qed.

(* Show that a bad_label_list is incompatible with a bound on the number of
   instructions to a cost label, by induction on the bound and the invariant
   that none of the instructions involved are a cost label. *)
    
lemma loop_soundness_contradiction_aux : ∀g,l1,l2,H1.
  Exists ? (λl.l = l2) (successors (lookup_present … g l1 H1)) →
  ¬ is_cost_label (lookup_present … g l1 H1) →
  bad_label_list g l1 l2 →
  ∀n,l'.
  bad_label_list g l1 l' →
  ¬ bound_on_instrs_to_cost' g l' n.
#g #l1 #l2 #H1 #SC1 #NCS1 #BLL2
#n elim n
[ #l #BLL % #BOUND
  cases (bound_zero … BOUND) #H' #ICS
  cases (bad_label_list_no_cost … BLL H1 NCS1) #H''
  >ICS *
| #m #IH #l #BLL % #BOUND
  cases (bound_step … BOUND) #H' *
  [ #ICS cases (bad_label_list_no_cost … BLL H1 NCS1) #H'' >ICS *
  | #EX_BOUND inversion BLL
    [ #E1 #E2 destruct
      lapply (IH l2 BLL2)
      lapply (EX_BOUND … SC1)
      @absurd
    | #l3 #l4 #H3 #SC2 #NCS3 #BLL4 #_ #E1 #E2 destruct
      lapply (IH l4 BLL4)
      cut (Exists ? (λl.l=l4) (successors (lookup_present … H3)))
      [ cases (memb_exists … SC2) #left * #right #E >E @Exists_mid % ]
      #SC2' lapply (EX_BOUND … SC2')
      @absurd
    ]
  ]
] qed.

lemma loop_soundness_contradiction : ∀g,l1,l2,H1.
  Exists ? (λl.l = l2) (successors (lookup_present … g l1 H1)) →
  ¬ is_cost_label (lookup_present … g l1 H1) →
  bad_label_list g l1 l2 →
  ∀n. ¬ bound_on_instrs_to_cost' g l2 n.
#g #l1 #l2 #H1 #EX #NCS #BLL #n
@(loop_soundness_contradiction_aux … BLL … BLL) //
qed.