Qcert.Basic.Logger.OptimizerStep

Section OptimizerStep.


  Record OptimizerStep (lang:Set) : Set :=
    mkOptimizerStep {
        optim_step_name : String.string
        ; optim_step_description : String.string
        ; optim_step_lemma : String.string
        ; optim_step_step (input:lang): lang
      }.


  Record OptimizerStepModel {lang:Set} (R:relation lang) :=
    mkOptimizerStepModel {
        optim_step_model_step : OptimizerStep lang
        ; optim_step_model_step_correct (input:lang): R input (optim_step_step optim_step_model_step input)
      }.



  Definition optim_model_list_complete {lang:Set} {R:relation lang}
             (optim_list:list (OptimizerStep lang))
             (optim_correct_list :list (OptimizerStepModel R))
    := ∀ x,
      In x optim_list →
      ∃ y,
        In y optim_correct_list
        ∧ optim_step_model_step _ y = x.

  Definition optim_list_correct {lang:Set} (R:relation lang)
             (optim_list:list (OptimizerStep lang))
    := Forall (fun o ⇒ ∀ input, R input (optim_step_step o input)) optim_list.

  Lemma optim_list_correct_from_model {lang:Set} {R:relation lang}
        {optim_list:list (OptimizerStep lang)}
        {optim_correct_list :list (OptimizerStepModel R)} :
    optim_model_list_complete optim_list optim_correct_list →
    optim_list_correct R optim_list.


  Definition optim_list_distinct {lang:Set}
             (optim_list:list (OptimizerStep lang))
    := NoDup (map optim_step_name optim_list).

  Lemma optim_list_distinct_dec {lang:Set}
        (optim_list:list (OptimizerStep lang))
    : {optim_list_distinct optim_list} + {¬ optim_list_distinct optim_list}.

  Definition optim_list_distinct_holds {lang:Set}
             (optim_list:list (OptimizerStep lang))
    := holds (optim_list_distinct_dec optim_list).

  Lemma optim_list_distinct_prover {lang:Set}
        (optim_list:list (OptimizerStep lang))
        (pf:optim_list_distinct_holds optim_list) :
    optim_list_distinct optim_list.

  Fixpoint optim_lookup {lang:Set}
           (optim_list:list (OptimizerStep lang)) (name:string)
    : option (OptimizerStep lang)
    := match optim_list with
       | nil ⇒ None
       | opt::rest ⇒
         if optim_step_name opt == name
         then Some opt
         else optim_lookup rest name
       end.

  Lemma optim_lookup_name_correct {lang:Set}
           (optim_list:list (OptimizerStep lang)) (name:string) (o:OptimizerStep lang)
    : optim_lookup optim_list name = Some o → optim_step_name o = name.

  Lemma optim_lookup_some_in {lang:Set}
           (optim_list:list (OptimizerStep lang)) (name:string) (o:OptimizerStep lang)
    : optim_lookup optim_list name = Some o → In o optim_list.

    Lemma optim_lookup_none_nin {lang:Set}
           (optim_list:list (OptimizerStep lang)) (name:string)
      : optim_lookup optim_list name = None →
        ∀ o, In o optim_list → optim_step_name o ≠ name.

  Definition optim_lookup_as_list {lang:Set}
           (optim_list:list (OptimizerStep lang)) (name:string)
    : list (OptimizerStep lang)
    := match optim_lookup optim_list name with
       | None ⇒ nil
       | Some res ⇒ res::nil
       end.

  Definition valid_optims {lang:Set}
           (optim_list:list (OptimizerStep lang)) (names:list string) :
    list string × list string
    := partition
         (fun x ⇒ if optim_lookup optim_list x then true else false)
         names .

  Definition project_optims {lang:Set}
           (optim_list:list (OptimizerStep lang)) (names:list string)
    := flat_map (optim_lookup_as_list optim_list) names.

  Lemma project_optims_incl {lang:Set}
        (optim_list:list (OptimizerStep lang)) (names:list string) :
    incl (project_optims optim_list names) optim_list.

  Lemma project_optims_model_list_complete {lang:Set} {R:relation lang}
        {optim_list:list (OptimizerStep lang)}
        {optim_correct_list:list (OptimizerStepModel R)}
        (pf:optim_model_list_complete optim_list optim_correct_list)
        (names:list string)
    : optim_model_list_complete
        (project_optims optim_list names)
        optim_correct_list.

    Lemma project_optims_list_correct {lang:Set} {R:relation lang}
        {optim_list:list (OptimizerStep lang)}
        (pf:optim_list_correct R optim_list)
        (names:list string)
    : optim_list_correct R
        (project_optims optim_list names).

End OptimizerStep.