text:
(* -*- company-coq-local-symbols: (("|=" . ?⊨) ("=|" . ?⫤) ("->>" . ?↠) ("=~" . ?≈) ("<|" . ?⟨) ("|>" . ?⟩) ); -*- *)
Set Warnings "-notation-overridden".

Require Import Prelude.Prelude.
Require Import Defs.Defs.
Require Import Wf.Wf.

Require Import Sound.Imi.
Require Import Sound.Umi.
Require Import Sound.Uu.

(*** Lemmas *)
Lemma Inst_to_SubSump : forall (dsub : DSub) (dsch : DSch) (dty : DTy) (denv : DEnv) (env : Env) (sch : Sch) (a : A) (ty : Ty),
    env |= sch ≤ ⟨a⟩ ty
  -> varl a [<=] DSub_dom dsub
  -> DSub_app_t ty dsub = emb_Ty dty
  -> DSub_app sch dsub = emb_Sch dsch
  -> DSub_wf denv dsub
  -> SubSump denv dsch (DS_Mono dty).
Proof.
  introv INST INS EMB__ty EMB__sch SUBWF. gen dty dsch denv. induction INST; intros.
  - emb_auto. rewrite EMB__ty in *. forwards: emb_Ty_inj. eassumption. crush.
  - do_DSub_exA_decide dsub exA.
    + (*exA is in sub so this can't be*)
      assert (exA \in DSub_dom dsub). rewrite <- INS. rewr. fsetdec. crush.
    + emb_auto. eapply (SubSumpInst (L \u DSub_codom_dskvars dsub)).
      * instantiate (1 := dty0). eauto.
      * intros. eapply H.
        -- instantiate (1 := dskA). fsetdec.
        -- rewrite <- INS. rewr. fsetdec.
        -- eassumption.
        -- assert (lc_DTy dty0). eauto.
           rewrite subst_skvar_Sch_open_Sch_wrt_Ty. 2:auto. rewrite subst_dskvar_DSch_open_DSch_wrt_DTy. 2:auto. simpl. if_taut.
           rewrite DSub_app_open_comm. 2,3:auto. rewrite embed_Sch_open_comm. rewrite EMB.
           rewrite DSub_app_susbst_skvar_Sch. 2:auto. rewrite embed_Sch_subst_dskvar_DSch. crush. eauto.
        -- auto.
Qed.

Lemma AInst_shift_DAin_to_produced_DEnv : forall (denv__init : DEnv) (da1 da2 : DA) (a : A) (dsub__init dsub : DSub),
    {denv__init :::a da1, dsub__init }a|= a ~> {da2, dsub}
  -> exists da,
    {denv__init, dsub__init }a|= a ~> {da, dsub}
  /\ da [<=]l (da1 ++ da2).
Proof.
  intros. gen da2 dsub. induction a; intros; inv_AInst.
  - exists (nil : DA). auto.
  - forwards [da [INST SUB]]: IHa. eassumption.
    econstructor. split.
    + econstructor. instantiate (1 := da). 2:assumption.
      instantiate (1 := da1 ++ DA2 ++ DA1). eapply WfDTy_DEnv_sub. eassumption.
      unfold DEnv_sub. unfold_DEnv_to_Set. progress (autorewrite with DEnv_to_Set List_to_Set). fold_DEnv_to_Set.
      fold DEnv_sub.
      rewr_derel.
      rewrite (fold_right_varl (DA2 ++ DA1)).
      rewrite (fold_right_varl (da1 ++ DA2 ++ DA1 ++ da)). rewr. fsetdec.
    + rewrite SUB. autounfold. rewr. fsetdec.
Qed.

Lemma generalize_Sch_generalize_DSch__helper : forall (L : vars) (dsub : DSub) (sch : Sch) (exA : exvar) (dsch : DSch),
    DSub_app (generalize_Sch sch [exA] empty) dsub = emb_Sch (DS_Forall dsch)
  -> (exists denv : DEnv, DSub_wf denv dsub)
  -> exists dskA,
    dskA `notin` L
  /\ DSub_app sch (dsub ++ [(exA, DT_SkVar_f dskA)]) = emb_Sch (open_DSch_wrt_DTy dsch (DT_SkVar_f dskA)).
Proof.
  introv EMB WFS. remember (proj1_sig (atom_fresh (free_skvars_Sch sch \u (L \u free_skvars_Sch (emb_Sch dsch) \u DSub_codom_dskvars dsub)))) as dskA.
  erewrite (generalize_Sch_l_irrelevance (L \u free_skvars_Sch (emb_Sch dsch) \u DSub_codom_dskvars dsub)) in EMB.
  forwards: proj1_sig_fresh (free_skvars_Sch sch \u (L \u free_skvars_Sch (emb_Sch dsch) \u DSub_codom_dskvars dsub)).
  exists dskA. split.
  - fsetdec.
  - eapply (close_Sch_wrt_Ty_inj _ _ dskA).
    subst. simpl in EMB. emb_auto. rewrite embed_Sch_open_comm. subdist. simpl.
    rewrite DSub_app_close_Sch_wrt_Ty in EMB. rewrite EMB.
    rewrite close_Sch_wrt_Ty_open_Sch_wrt_Ty. reflexivity.
    forwards: proj1_sig_fresh (free_skvars_Sch sch \u (free_skvars_Sch (emb_Sch dsch) \u DSub_codom_dskvars dsub)).
    crush. fsetdec. eassumption.
Qed.

Inductive DA_for_A : DA -> A -> DSub -> Prop :=    (* defn DFrA *)
 | DA_for_A_nil  : DA_for_A (nil : DA) (nil : A) (nil : DSub)
 | DA_for_A_cons : forall (dskA:dskvar) (exA:exvar) (DA:DA) (A:A) (DSub:DSub)
     (DA_rec: DA_for_A DA A DSub),
     DA_for_A (cons dskA DA) (cons exA A) (((exA, DT_SkVar_f dskA)) :: DSub).
#[export] Hint Constructors DA_for_A : core.

Lemma generalize_Sch_generalize_DSch : forall (sch : Sch) (a : A) (dsch2 : DSch) (dsub : DSub) (denv : DEnv),
    DSub_app (generalize_Sch sch a empty) dsub = emb_Sch dsch2
  -> DSub_wf denv dsub
  -> (exists (env : Env), FrA a env /\ DSub_dom dsub [<=] Env_exvars env)
  -> exists dsch1 da dsub',
      generalize_DSch dsch1 da = dsch2
    /\ DSub_app sch (dsub ++ dsub') = emb_Sch dsch1
    /\ DA_for_A da a dsub'
    /\ DSub_wf (denv :::a da) (dsub ++ dsub')
    /\ DFrA da denv.
Proof.
  introv EMB WFS FR.
  gen denv dsub dsch2. listind a; intros.
  - simpl in EMB. exists dsch2 (nil:DA) (nil:DSub). crush.
  - rewrite generalize_sch_cons in EMB.
    assert (EQ__dsch2 : exists dsch2', dsch2 = DS_Forall dsch2'). simpl in EMB. emb_auto. exists. auto.
      destruct EQ__dsch2 as [dsch2' ?]. subst.
    forwards [dskA [NIV EMB']]: generalize_Sch_generalize_DSch__helper (free_dskvars_DSch dsch2' \u DEnv_dskvars denv). eassumption. exists denv. assumption.
    destruct FR as [env [FrA SUB__env]].
    forwards dsch1 da dsub' GEN__IH [EMB__IH [DAFORA__IH [WF__dsub DFR]]]: IHa. 3:eassumption. instantiate (1 := denv :::s dskA).
    apply DSub_wf_snoc. eauto. eapply in_disjoint_impl_notin1. symmetry.
    rewrite SUB__env. conv. apply FrA_props. eassumption. rewr. fsetdec. constructor. rewr. fsetdec.
    exists (env ::a [exA]). split. apply FrA_cons_shift. assumption. rewr. crush.
    eexists. exists (dskA :: da). exists ((exA, DT_SkVar_f dskA) :: dsub'). splits.
    + rewrite generalize_DSch_cons. rewrite GEN__IH. simpl.
      rewrite close_DSch_wrt_DTy_open_DSch_wrt_DTy. reflexivity. fsetdec.
    + rewr in EMB__IH. eassumption.
    + crush.
    + eapply DSub_wf_rewr. eassumption. rewr_derel. rewrite (fold_right_varl (dskA :: da)). rewr. fsetdec. rewr. fsetdec.
    + apply DFrA_cons_shift. eassumption. fsetdec.
Qed.

Lemma DA_for_A_AInst : forall DEnv__init DSub__init DA A DSub,
    DA_for_A DA A DSub
  -> {DEnv__init, DSub__init }a |= A ~> {DA, DSub}.
Proof.
  intros DEnv__init DSub__init DA A DSub DAFA. induction DAFA. auto.
  applys_eq AInstCons. norm. reflexivity. constructor. rewr. fsetdec. assumption.
Qed.

Lemma DA_for_A_DSub_dom : forall da a dsub,
    DA_for_A da a dsub
  -> DSub_dom dsub [=] varl a.
Proof. introv DAforA. induction DAforA; crush. Qed.

(*** Main theorem *)
Definition Inf_sound__def := forall (env__in : Env) (e : e) (a : A) (ty : Ty) (env__out : Env) (denv : DEnv) (dty : DTy),
    env__in |= e ▸ ⟨a⟩ ty =| env__out
  -> wf(env__in)
  -> FullEInst ((env__out ::a a) ::o ⟦S_Mono ty⟧) (denv :::o ⟦DS_Mono dty⟧d)
  -> denv |=m e ▸ dty.
Definition Inf_sound__prop (env__in : Env) (e : e) (a : A) (ty : Ty) (env__out : Env)
                          (inf : env__in |= e ▸ ⟨a⟩ ty =| env__out) : Prop := forall (denv : DEnv) (dty : DTy),
    wf(env__in)
  -> FullEInst ((env__out ::a a) ::o ⟦S_Mono ty⟧) (denv :::o ⟦DS_Mono dty⟧d)
  -> denv |=m e ▸ dty.
#[local] Hint Unfold Inf_sound__def Inf_sound__prop : core.

Definition Gen_sound__def := forall (env__in : Env) (e : e) (sch: Sch) (env__out : Env) (denv : DEnv) (dsch : DSch),
    env__in |= e ▸ sch =| env__out
  -> wf(env__in)
  -> FullEInst (env__out ::o ⟦sch⟧) (denv :::o ⟦dsch⟧d)
  -> denv |=p e ▸ dsch.
Definition Gen_sound__prop (env__in : Env) (e : e) (sch: Sch) (env__out : Env)
                          (gen : env__in |= e ▸ sch =| env__out) : Prop := forall (denv : DEnv) (dsch : DSch),
    wf(env__in)
  -> FullEInst (env__out ::o ⟦sch⟧) (denv :::o ⟦dsch⟧d)
  -> denv |=p e ▸ dsch.
#[local] Hint Unfold Gen_sound__def Gen_sound__prop : core.

Theorem EInst_WfTy_partial_DSub_app : forall (sch : Sch) (dsch : DSch) (env : Env) (denv : DEnv) (dsub dsub' : DSub),
    {▪, []}|= env ~> {denv, dsub}
  -> DSub_app sch (dsub' ++ dsub) = emb_Sch dsch
  -> env |=ty sch
  -> DSub_app sch           dsub  = emb_Sch dsch
  /\ denv |=dty dsch.
Proof.
  introv INST EMB WFTY.
  forwards [dsch' [EMB' WFDTY]]: EInst_WfTy_impl_emb. eassumption. eassumption.
  subdist in EMB. rewrite EMB' in EMB. rewr in EMB. apply emb_Sch_inj in EMB. crush.
Qed.

Corollary EInst_WfTy_partial_DSub_app_Ty : forall (ty : Ty) (dty : DTy) (env : Env) (denv : DEnv) (dsub dsub' : DSub),
    DSub_app_t ty (dsub' ++ dsub) = emb_Ty dty
  -> {▪, []}|= env ~> {denv, dsub}
  -> env |=ty (S_Mono ty)
  -> DSub_app_t ty           dsub  = emb_Ty dty.
Proof. introv EMB INST WFTY. forwards: EInst_WfTy_partial_DSub_app (S_Mono ty) (DS_Mono dty). eassumption. crush. eassumption. crush. Qed.

Theorem Inf_Gen_sound : Inf_sound__def /\ Gen_sound__def.
Proof.
  forwards: (Inf_Gen_mut Inf_sound__prop Gen_sound__prop)
  ; unfold Inf_sound__prop in *; unfold Gen_sound__prop in *
  .
  7:{ jauto. }

  (** var case*)
  - introv IN INSTANT WF [dsub INST].
    (**)
    forwards WF1 : Inf_Wf. econstructor; eauto. assumption.
    (**)
    EInst_props. eassumption. inv_Wf. constructor. eauto. auto. eauto. auto. crush.
    forwards [dsch [EMB IN']]: IN__sch Sch5. rewr. eauto. rewr in IN'.
    (**)
    applys TmVar dsch. eassumption.
    (**)
    inv_EInst'. eapply (Inst_to_SubSump (DSub2 ++ DSub1)). eassumption. 2,3:crush.
    + forwards [_ [_ EQ__A]]: AInst_props__base. eassumption.
      unfold DSub_dom. subst. rewr. fsetdec.
    + eapply DSub_wf_rewr. 3:reflexivity. rewr in WF__dsub. eassumption. rewr_derel. reflexivity.

  (** unit case*)
  - introv _ _ [dsub INST]. inv_EInst'. rewr*. emb_auto. crush.

  (** let case*)
  - introv FR INF IH WF__in [dsub INST].
    (**)
    (**)
    fresh_atom.
    (** We need the same with x' later*)
    forwards WF__out: Inf_Wf. eapply INF. eassumption. do 2 constructor. assumption. constructor. auto. crush. crush.
    (**)
    inv_EInst'. rewr*. emb_auto.
    (**)
    EInst_props__base. eapply EInstA. eassumption. apply AInst_merge; rewr; eassumption. rewr in SUB__wfdty.
    (**)
    econstructor.
    + forwards [FV__sk [_ LC]]: WfTy_props_mono1 (Envout ::a (A2 ++ A1)). inv_Wf. eapply WfTy_Env_sub. eassumption. eauto.
      eapply embed_Ty_WfDTy. eassumption. rewr. eassumption. rewrite <- SUB__sk.
      eassumption. eassumption.
    + intros x' NIL'. rewrite DEnv_cons_da_app_split. apply Mon_shift_DA. eapply IH. eassumption.
      do 2 constructor. assumption. constructor. auto. crush. crush.
      eexists. econstructor. constructor. constructor. constructor. all: rewr. 1,2: eassumption. 3,4:crush.
      * rewr.
        forwards EMB1': EInst_WfTy_partial_DSub_app_Ty Ty1 (dsub ++ DSub1) dsub0.
          eassumption. eapply EInstA. eassumption. rewr. eassumption. eauto.
        crush.
      * rewr. eapply AInst_init_DEnv_sub. eassumption. crush.

  (** app case*)
  - introv FR INF__e1 IH__e1 INF__e2 IH__e2 UNI WF__in [dsub INST__out].
    (**)
    forwards WF1: Inf_Wf. apply INF__e1. assumption. inv_Wf. rename WF into WF1.
    forwards WF2: Inf_Wf. apply INF__e2. eauto. inv_Wf. rename WF0 into WF2.
    rename Ty_5 into ty. rename Ty1 into ty1. rename Ty' into ty'. rename Ty2 into ty2.
    (**)
    forwards [ty__uni UNI']: U_unifies. eassumption.
    (**)
    assert (WF2': wf((((Env2 ::a (exB :: A2 ++ A1')) ::o ⟦⟨[]⟩ S_Mono (T_ExVar exB)⟧) ::o ⟦⟨[]⟩ S_Mono ty'⟧) ::o ⟦⟨[]⟩ S_Mono (T_Fun ty1 (T_ExVar exB))⟧)).
    { econstructor. 2:auto. constructor. 2:auto. econstructor. 2:auto. econstructor. assumption.
      - constructor. apply FrA_app_split. split. erewrite <- FrA_Obj. eauto. eassumption. crush.
      - constructor. crush.
      - eapply WfTy_Env_sub. eassumption. autounfold. rewr. crush.
      - constructor. eapply WfTy_Env_sub. eassumption. autounfold. rewr. crush. constructor. crush.
    }
    (**)
    forwards WF__out: U_Wf. apply UNI'. assumption.
    (**)
    forwards [dsch [EMB WFDTY]]: EInst_WfTy_impl_emb (S_Mono ty__uni). eassumption.
    inv_Wf. eapply WfTy_Env_sub. eassumption. rewr_erel. fsetdec.
    destruct dsch as [dty'|?]. 2:inverts EMB. emb_auto.
    (**)
    forwards [?dsub INST2]: unification_maintains_instantiation.
      { apply UNI'. }
      { exists. econstructor.
        - econstructor. eauto. auto. instantiate (1 := DS_Mono dty'). rewr. crush.
        - auto.
        - instantiate (1 := DS_Mono dty'). rewr. crush.
      }
      assumption.
    forwards [_ [_ [_ [_ SUB__wf]]]]: EInst_props. apply INST2. eauto. auto. crush. rewr in SUB__wf.
    inv_EInst'. rewr*. emb_auto.
    (**)
    norm in EMB1. rewrite app_assoc in EMB1. eapply EInst_WfTy_partial_DSub_app_Ty in EMB1.
    2:{ eapply EInstA. eassumption. rewr. eassumption. }
    2:{ eassumption. }
    (**)
    norm in EMB5. rewrite (DSub_unique_sub_DSub_app_t _ ([(exB, DTy5)] ++ dsub ++ dsub0 ++ DSub0)) in EMB5.
    2:{ apply DSub_full_t_emb. exists. eassumption. }
    2:{ rewr_dsrel. fsetdec'. }
    2:{ unfold DSub_unique. introv IN1 IN2. eapply SUB__wf. instantiate (1 := exA).
        rewr_derel. rewr_derel in IN1. fsetdec'.
        rewr_derel. rewr_derel in IN2. fsetdec'. }
    rewrite app_assoc in EMB5.
    forwards [da0' [?INST SUB]]: AInst_shift_DAin_to_produced_DEnv. apply INSTA0. eapply EInst_WfTy_partial_DSub_app_Ty in EMB5.
    2:{ apply EInstA. eassumption. rewr. eapply AInst_swap_subinit. eassumption. }
    2:{ eapply WfTy_Env_sub. eassumption. rewr_erel. fsetdec. }
    (**)
    assert (dty = dty2). destruct (eq_Ty (emb_Ty dty) (emb_Ty dty2)). eauto using emb_Ty_inj. crush. subst.
    (**)
    forwards [?dsub INST2]: inference_maintains_instantiation. apply INF__e2. constructor; auto.
      exists. econstructor. eauto. rewr. eassumption. rewr. instantiate (1 := DS_Mono (DT_Fun dty1 dty2)). crush.
    (**)
    eapply (TmApp _ _ _ _ dty1).
    (* assert ((DEnv_0 :::a (DA2 ++ da0 ++ da)) |=m e1 ▸ DT_Fun dty1 dty2). *)
    +
      inv_EInst'.
      eapply Mon_DEnv_x_sub. eapply IH__e1. auto.
        exists. inv_EInst'. rewr*. econstructor. econstructor. eassumption. rewr. apply INSTA1. auto. rewr. assumption.
        autounfold. split. rewr. rewrite (fold_right_varl (DA2 ++ da0 ++ da)). rewr. fsetdec. rewr. crush.
    + eapply Mon_DEnv_x_sub. eapply (IH__e2 (DEnv_0 :::o ⟦⟨da⟩ DS_Mono (DT_Fun dty1 dty2)⟧d :::a da0')). eauto.
      * exists. econstructor. econstructor. econstructor. eassumption. rewr. eassumption. rewr. rewrite EMB1. reflexivity.
        rewr. eapply AInst_swap_subinit. eapply AInst_init_DEnv_sub. eassumption. crush. auto. rewr. crush.
      * autounfold. split. rewr. autounfold in SUB. rewrite SUB. rewr. rewrite (fold_right_varl (DA2 ++ da0 ++ da)). rewr. fsetdec.
        rewr. crush.

  (** let case *)
  - introv POL IH__e1 INF IH__e2 WF1 [dsub INST__out].
    forwards [x NIL__x]: atom_fresh.
    (**)
    forwards WF2: Gen_Wf. eassumption. assumption.
    (**)
    forwards WF__out: Inf_Wf. eapply INF. eassumption. eauto with slow.
    inv_EInst'. inv_Wf. rewr*.
    (**)
    forwards [dsch' [EMB' WFDTY]]: EInst_WfTy_impl_emb. 2:apply WFTY0. eassumption.
    (**)
    econstructor.
    + forwards [dsub INST__mid]: inference_maintains_instantiation. eapply INF. eassumption. eapply wf_Env_Obj_noa_x1. auto.
        exists. econstructor. eassumption. rewr. eassumption. inv_EInst'. rewr*.
      eapply DGen_DEnv_x_sub. apply IH__e1. auto. exists. econstructor. eassumption. auto. rewr. eassumption. auto.
    + intros y NIL__y.
      (** This usage of Mon_DEnv_x_sub just reshuffles *)
      eapply Mon_DEnv_x_sub. eapply IH__e2. eassumption. eauto.
      exists. econstructor. econstructor. econstructor. eassumption. rewr. eassumption. rewr.
      eapply AInst_init_DEnv_sub. eassumption. eauto. auto. rewr. eassumption. autounfold.
      (** reshuffeling here *)
      split. rewr. fsetdec. rewr_dsrel. fsetdec'.

  (** generalization case *)
  - introv INF IH GEN WF__in [dsub INST__out].
    forwards WF__out: Inf_Wf. eassumption. assumption. inv_Wf.
    inv_EInst'. rewr*. subst.
    EInst_props. eassumption. auto. auto. crush. rewr*.
    (**)
    forwards [dsch' [da [dsub' [GEN [AFORA [EMB' [WF__dusb' DFR]]]]]]]: generalize_Sch_generalize_DSch denv. eassumption. eauto. exists Envout. crush.
    emb_auto.
    (**)
    eapply TmGen. 3:{ reflexivity. } eassumption. apply IH. auto.
    exists. econstructor. econstructor. eassumption. rewr.
    eauto using DA_for_A_AInst. auto. rewr.
    rewrite DSub_app_t_app_symm. 2:{ apply DSub_unique_app_symm. eauto. }
    crush.
Qed.

Theorem Soundness__mono : forall (e : e) (a : A) (ty : Ty) (dty : DTy),
    • |= e ▸ ⟨a⟩ ty =| •
  -> FullEInst (<a>a ::o ⟦S_Mono ty⟧) <⟦DS_Mono dty⟧d>do
  -> ▪ |=m e ▸ dty.
Proof.
  introv Inf [dsub INST]. forwards S : proj1 Inf_Gen_sound. unfold Inf_sound__def in S.
  forwards: S ▪. eassumption. auto. exists dsub. eassumption. eassumption.
Qed.

Theorem Soundness__poly : forall (e : e) (sch : Sch) (dsch : DSch),
    • |= e ▸ sch =| •
  -> FullEInst <⟦sch⟧>o <⟦dsch⟧d>do
  -> ▪ |=p e ▸ dsch.
Proof.
  introv Gen [dsub INST]. forwards S : proj2 Inf_Gen_sound. unfold Inf_sound__def in S.
  forwards: S ▪. eassumption. auto. exists dsub. eassumption. eassumption.
Qed.

author: rogerbosman

repo: hdm-fully-grounding

sha: master


text:
Load LFindLoad.
From lfind Require Import LFind.
Unset Printing Notations.
Set Printing Implicit.

From QuickChick Require Import QuickChick.
Inductive natural : Type := Succ : natural -> natural |  Zero : natural.
Derive Show for natural. Derive Arbitrary for natural.  Instance Dec_Eq_natural : Dec_Eq natural. Proof. dec_eq. Qed.
Inductive lst : Type :=  Nil : lst | Cons : natural -> lst -> lst .

Inductive tree : Type := Node : natural -> tree -> tree -> tree |  Leaf : tree.

Inductive Pair : Type := mkpair : natural -> natural -> Pair
with Zlst : Type := zcons : Pair -> Zlst -> Zlst |  znil : Zlst.

Fixpoint append (append_arg0 : lst) (append_arg1 : lst) : lst
           := match append_arg0, append_arg1 with
              | Nil, x => x
              | Cons x y, z => Cons x (append y z)
              end.

Fixpoint rev (rev_arg0 : lst) : lst
           := match rev_arg0 with
              | Nil => Nil
              | Cons x y => append (rev y) (Cons x Nil)
              end.

Lemma append_nil : forall (x : lst), append x Nil = x.
Proof.
   intros.
   induction x.
   - reflexivity.
   - simpl. rewrite IHx. reflexivity.
Qed.

Lemma append_assoc : forall (x y z : lst), append (append x y) z = append x (append y z).
Proof.
   intros.
   induction x.
   - reflexivity.
   - simpl. rewrite IHx. reflexivity.
Qed.

Lemma rev_append : forall (x y : lst), rev (append x y) = append (rev y) (rev x).
Proof.
   intros.
   induction x.
   - simpl. rewrite append_nil. reflexivity.
   - simpl. rewrite IHx. rewrite append_assoc. reflexivity.
Qed.

Lemma rev_rev : forall (x : lst), rev (rev x) = x.
Proof.
   intros.
   induction x.
   - reflexivity.
   - simpl. lfind. Admitted.

author: ana-brendel

repo: coq-benchmarks


text:
From isla Require Import opsem.

Definition a1c : isla_trace :=
  Smt (DeclareConst 50%Z (Ty_BitVec 64%N)) Mk_annot :t:
  ReadReg "R2" [] (RegVal_Base (Val_Symbolic 50%Z)) Mk_annot :t:
  Smt (DefineConst 56%Z (Manyop (Bvmanyarith Bvor) [Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot; Val (Val_Symbolic 50%Z) Mk_annot] Mk_annot)) Mk_annot :t:
  WriteReg "R20" [] (RegVal_Base (Val_Symbolic 56%Z)) Mk_annot :t:
  Smt (DeclareConst 57%Z (Ty_BitVec 64%N)) Mk_annot :t:
  ReadReg "_PC" [] (RegVal_Base (Val_Symbolic 57%Z)) Mk_annot :t:
  Smt (DefineConst 58%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 57%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
  WriteReg "_PC" [] (RegVal_Base (Val_Symbolic 58%Z)) Mk_annot :t:
  tnil
.

author: rems-project

repo: islaris

save_path: github-repos/coq/rems-project-islaris


text:
(* --------------------------------------------------------------------
 * Copyright (c) - 2006--2012 - IMDEA Software Institute
 * Copyright (c) - 2006--2012 - Inria
 * Copyright (c) - 2006--2012 - Microsoft Coprporation
 *
 * Distributed under the terms of the CeCILL-B-V1 license
 * -------------------------------------------------------------------- *)

(*************************************************************)
(*      This file is distributed under the terms of the      *)
(*      GNU Lesser General Public License Version 2.1        *)
(*************************************************************)
(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
(*************************************************************)

Require Import List.
Require Import ZArith.
Require Import Zorder.
Require Import ZCAux.
Require Import LucasLehmer.
Require Import Pocklington.
Require Import ZArith Znumtheory Zpow_facts.
Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31.
Require Import Pmod.
Require Import Mod_op.
Require Import W.
Require Import Lucas.
Require Export PocklingtonCertificat.
Require Import NEll.
Import CyclicAxioms DoubleType DoubleBase List.

Open Scope Z_scope.

Section test.

Variable w: Type.
Variable w_op: znz_op w.
Variable op_spec: znz_spec w_op.
Variable p: positive.
Variable b: w.

Notation "[| x |]" :=
   (znz_to_Z w_op x)  (at level 0, x at level 99).

Hypothesis b_pos: 0 < [|b|].

Variable m_op: mod_op w.
Variable m_op_spec: mod_spec w_op b m_op.

Open Scope positive_scope.
Open Scope P_scope.

Let pow := m_op.(power_mod).
Let times := m_op.(mul_mod).
Let pred:= m_op.(pred_mod).

(* [fold_pow_mod a [q1,_;...;qn,_]] b = a ^(q1*...*qn) mod b *)
(* invariant a mod N = a *)
Definition fold_pow_mod (a: w) l :=
  fold_left
    (fun a' (qp:positive*positive) =>  pow a' (fst qp))
    l a.

Lemma fold_pow_mod_spec : forall l (a:w),
  ([|a|] < [|b|])%Z -> [|fold_pow_mod a l|] = ([|a|]^(mkProd' l) mod [|b|])%Z.
intros l; unfold fold_pow_mod; elim l; simpl fold_left; simpl mkProd'; auto; clear l.
intros a H; rewrite Zpower_1_r; rewrite Zmod_small; auto with zarith.
case (spec_to_Z op_spec a); auto with zarith.
intros (p1, q1) l Rec a H.
case (spec_to_Z op_spec a); auto with zarith; intros U1 U2.
rewrite Rec.
rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith.
rewrite <- Zpower_mod.
rewrite times_Zmult; rewrite Zpower_mult; auto with zarith.
apply Zle_lt_trans with (2 := H); auto with zarith.
rewrite Zmod_small; auto with zarith.
rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith.
match goal with |- context[(?X mod ?Y)%Z] =>
  case (Z_mod_lt X Y); auto with zarith
end.
rewrite Zmod_small; auto with zarith.
Qed.

Fixpoint all_pow_mod (prod a: w) (l:dec_prime) {struct l}: w*w :=
  match l with
  | nil => (prod,a)
  | (q,_) :: l =>
    let m := pred (fold_pow_mod a l) in
    all_pow_mod (times prod m) (pow a q) l
  end.

Lemma snd_all_pow_mod :
 forall l (prod a :w), ([|a|] < [|b|])%Z ->
   [|snd (all_pow_mod prod a l)|] = ([|a|]^(mkProd' l) mod [|b|])%Z.
intros l; elim l; simpl all_pow_mod; simpl mkProd'; simpl snd; clear l.
intros _ a H; rewrite Zpower_1_r; auto with zarith.
rewrite Zmod_small; auto with zarith.
case (spec_to_Z op_spec a); auto with zarith.
intros (p1, q1) l Rec prod a H.
case (spec_to_Z op_spec a); auto with zarith; intros U1 U2.
rewrite Rec; auto with zarith.
rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith.
rewrite <- Zpower_mod.
rewrite times_Zmult; rewrite Zpower_mult; auto with zarith.
apply Zle_lt_trans with (2 := H); auto with zarith.
rewrite Zmod_small; auto with zarith.
rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith.
match goal with |- context[(?X mod ?Y)%Z] =>
  case (Z_mod_lt X Y); auto with zarith
end.
rewrite Zmod_small; auto with zarith.
Qed.

Lemma fold_aux : forall a N l prod,
  (fold_left
     (fun (r : Z) (k : positive * positive) =>
      r * (a ^(N / fst k) - 1) mod [|b|]) l (prod mod [|b|]) mod [|b|] =
  fold_left
     (fun (r : Z) (k : positive * positive) =>
      r * (a^(N / fst k) - 1)) l prod mod [|b|])%Z.
induction l;simpl;intros.
rewrite Zmod_mod; auto with zarith.
rewrite <- IHl; auto with zarith.
rewrite Zmult_mod; auto with zarith.
rewrite Zmod_mod; auto with zarith.
rewrite <- Zmult_mod; auto with zarith.
Qed.

Lemma fst_all_pow_mod :
 forall l (a:w) (R:positive) (prod A :w),
  [|prod|] = ([|prod|] mod [|b|])%Z ->
  [|A|] = ([|a|]^R mod [|b|])%Z ->
  [|fst (all_pow_mod prod A l)|] =
    ((fold_left
      (fun r (k:positive*positive) =>
        (r * ([|a|] ^ (R* mkProd' l / (fst k)) - 1))) l [|prod|]) mod [|b|])%Z.
intros l; elim l; simpl all_pow_mod; simpl fold_left; simpl fst;
  auto with zarith; clear l.
intros (p1,q1) l Rec; simpl fst.
intros a R prod A H1 H2.
assert (F: (0 <= [|A|] < [|b|])%Z).
rewrite H2.
match goal with |- context[(?X mod ?Y)%Z] =>
  case (Z_mod_lt X Y); auto with zarith
end.
assert (F1: ((fun x => x = x mod [|b|])%Z [|fold_pow_mod A l|])).
rewrite Zmod_small; auto.
rewrite fold_pow_mod_spec; auto with zarith.
match goal with |- context[(?X mod ?Y)%Z] =>
  case (Z_mod_lt X Y); auto with zarith
end.
assert (F2: ((fun x => x = x mod [|b|])%Z [|pred (fold_pow_mod A l)|])).
rewrite Zmod_small; auto.
rewrite(fun x => m_op_spec.(pred_mod_spec) x [|x|]);
  auto with zarith.
match goal with |- context[(?X mod ?Y)%Z] =>
  case (Z_mod_lt X Y); auto with zarith
end.
rewrite (Rec a (R * p1)%positive); auto with zarith.
rewrite(fun x y => m_op_spec.(mul_mod_spec) x y [|x|] [|y|]);
  auto with zarith.
rewrite(fun x => m_op_spec.(pred_mod_spec) x [|x|]);
  auto with zarith.
rewrite fold_pow_mod_spec; auto with zarith.
rewrite H2.
repeat rewrite Zpos_mult.
repeat rewrite times_Zmult.
repeat rewrite <- Zmult_assoc.
apply sym_equal; rewrite <- fold_aux; auto with zarith.
apply sym_equal; rewrite <- fold_aux; auto with zarith.
eq_tac; auto.
match goal with |- context[fold_left ?x  _ _] =>
  apply f_equal2 with (f := fold_left x); auto with zarith
end.
rewrite Zmod_mod; auto with zarith.
rewrite (Zmult_comm R); repeat rewrite <- Zmult_assoc;
 rewrite (Zmult_comm p1); rewrite Z_div_mult; auto with zarith.
repeat rewrite (Zmult_mod [|prod|]);auto with zmisc.
eq_tac; [idtac | eq_tac]; auto.
eq_tac; auto.
rewrite Zmod_mod; auto.
repeat rewrite (fun x => Zminus_mod x 1); auto with zarith.
eq_tac; auto; eq_tac; auto.
rewrite Zmult_comm; rewrite <- Zpower_mod; auto with zmisc.
rewrite Zpower_mult; auto with zarith.
rewrite Zmod_mod; auto with zarith.
rewrite Zmod_small; auto.
rewrite(fun x y => m_op_spec.(mul_mod_spec) x y [|x|] [|y|]);
  auto with zarith.
match goal with |- context[(?X mod ?Y)%Z] =>
  case (Z_mod_lt X Y); auto with zarith
end.
rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]);
  auto with zarith.
apply trans_equal with ([|A|] ^ p1 mod [|b|])%Z; auto.
rewrite H2.
rewrite Zpos_mult_morphism; rewrite Zpower_mult; auto with zarith.
rewrite <- Zpower_mod; auto with zarith.
rewrite Zmod_small; auto.
Qed.

Fixpoint pow_mod_pred (a:w) (l:dec_prime) {struct l} : w :=
  match l with
  | nil => a
  | (q, p)::l =>
    if (p ?= 1) then pow_mod_pred a l
    else
      let a' := iter_pos (Ppred p) _ (fun x => pow x q) a in
      pow_mod_pred a' l
  end.

Lemma iter_pow_mod_spec : forall q p a, [|a|] = ([|a|] mod [|b|])%Z ->
  ([|iter_pos p _ (fun x => pow x q) a|] = [|a|]^q^p mod [|b|])%Z.
intros q1 p1; elim p1; simpl iter_pos; clear p1.
intros p1 Rec a Ha.
rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]);
  auto with zarith.
repeat rewrite Rec; auto with zarith.
match goal with |- (Zpower_pos ?X ?Y mod ?Z = _)%Z =>
  apply trans_equal with (X ^ Y mod Z)%Z; auto
end.
repeat rewrite <- Zpower_mod; auto with zmisc.
repeat rewrite <- Zpower_mult; auto with zmisc.
repeat rewrite <- Zpower_mod; auto with zmisc.
repeat rewrite <- Zpower_mult; auto with zarith zmisc.
eq_tac; auto.
eq_tac; auto.
rewrite Zpos_xI.
assert (tmp: forall x, (2 * x = x + x)%Z); auto with zarith; rewrite tmp;
  clear tmp.
repeat rewrite Zpower_exp; auto with zarith.
rewrite Zpower_1_r; try ring; auto with misc.
rewrite Zmod_mod; auto with zarith.
rewrite Rec; auto with zmisc.
rewrite Zmod_mod; auto with zarith.
rewrite Rec; auto with zmisc.
rewrite Zmod_mod; auto with zarith.
intros p1 Rec a Ha.
repeat rewrite Rec; auto with zarith.
repeat rewrite <- Zpower_mod; auto with zmisc.
repeat rewrite <- Zpower_mult; auto with zmisc.
eq_tac; auto.
eq_tac; auto.
rewrite Zpos_xO.
assert (tmp: forall x, (2 * x = x + x)%Z); auto with zarith; rewrite tmp;
  clear tmp.
repeat rewrite Zpower_exp; auto with zarith.
rewrite Zmod_mod; auto with zarith.
intros a Ha; rewrite Zpower_1_r; auto with zarith.
rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]);
  auto with zarith.
Qed.

Lemma pow_mod_pred_spec : forall l a,
  ([|a|] = [|a|] mod [|b|] ->
  [|pow_mod_pred a l|] = [|a|]^(mkProd_pred l) mod [|b|])%Z.
intros l; elim l; simpl pow_mod_pred; simpl mkProd_pred; clear l.
intros; rewrite Zpower_1_r; auto with zarith.
intros (p1,q1) l Rec a H; simpl snd; simpl fst.
case (q1 ?= 1)%P; auto with zarith.
rewrite Rec; auto.
rewrite iter_pow_mod_spec; auto with zarith.
rewrite times_Zmult; rewrite pow_Zpower.
rewrite <- Zpower_mod; auto with zarith.
rewrite Zpower_mult; auto with zarith.
rewrite Zmod_small; auto with zarith.
rewrite iter_pow_mod_spec; auto with zarith.
match goal with |- context[(?X mod ?Y)%Z] =>
  case (Z_mod_lt X Y); auto with zarith
end.
Qed.

End test.

Require Import Bits.

Definition test_pock N a dec sqrt :=
  if (2 ?< N) then
    let Nm1 := Ppred N in
    let F1 := mkProd dec in
    match (Nm1 / F1)%P with
    | (Npos R1, N0) =>
      if is_odd R1 then
        if is_even F1 then
          if (1 ?< a) then
            let (s,r') := (R1 / (xO F1))%P in
            match r' with
            | Npos r =>
              if (a ?< N) then
              let op := cmk_op (pred (nat_of_P (get_height 31 (plength N)))) in
              let wN := znz_of_Z op (Zpos N) in
              let wa := znz_of_Z op (Zpos a) in
              let w1 := znz_of_Z op 1 in
              let mod_op := make_mod_op op wN in
              let pow := mod_op.(power_mod) in
              let ttimes := mod_op.(mul_mod) in
              let pred:= mod_op.(pred_mod) in
              let gcd:= op.(znz_gcd) in
              let A := pow_mod_pred _ mod_op (pow wa R1) dec in
              match all_pow_mod _ mod_op w1 A dec with
              | (p, aNm1) =>
                match znz_to_Z op aNm1 with
                  (Zpos xH) =>
                   match znz_to_Z op (gcd p wN) with
                   (Zpos xH) =>
                    if check_s_r s r sqrt then
		      (N ?< (times ((times ((xO F1)+r+1) F1) + r) F1) + 1)
                    else false
                   | _ => false
                   end
                 | _ => false
                end
              end else false
            | _ => false
            end
	  else false
        else false
      else false
    | _=> false
    end
  else false.

Lemma test_pock_correct : forall N a dec sqrt,
   (forall k, In k dec -> prime (Zpos (fst k))) ->
   test_pock N a dec sqrt = true ->
   prime N.
unfold test_pock;intros N a dec sqrt H.
match goal with |- context[if ?x then _ else _] =>
  case_eq x; intros If1; auto
end.
2: intros; discriminate.
match goal with H: (?X ?< ?Y) = true |- _ =>
  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
end.
generalize (div_eucl_spec (Ppred N) (mkProd dec));
 destruct ((Ppred N) / (mkProd dec))%P as (R1,n).
simpl fst; simpl snd; intros (H1, H2).
destruct R1 as [|R1].
intros; discriminate.
destruct n.
2: intros; discriminate.
match goal with |- context[if ?x then _ else _] =>
  case_eq x; intros If2; auto
end.
assert (If0: Zodd R1).
apply is_odd_Zodd; auto.
clear If2; rename If0 into If2.
2: intros; discriminate.
match goal with |- context[if ?x then _ else _] =>
  case_eq x; intros If3; auto
end.
assert (If0: Zeven (mkProd dec)).
apply is_even_Zeven; auto.
clear If3; rename If0 into If3.
2: intros; discriminate.
match goal with |- context[if ?x then _ else _] =>
  case_eq x; intros If4; auto
end.
match goal with H: (?X ?< ?Y) = true |- _ =>
  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
end.
2: intros; discriminate.
generalize (div_eucl_spec R1 (xO (mkProd dec)));
 destruct ((R1 / xO (mkProd dec))%P) as (s,r'); simpl fst;
 simpl snd; intros (H3, H4).
destruct r' as [|r].
intros; discriminate.
match goal with |- context[if ?x then _ else _] =>
  case_eq x; intros If5; auto
end.
match goal with H: (?X ?< ?Y) = true |- _ =>
  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
end.
2: intros; discriminate.
set (bb := pred (nat_of_P (get_height 31 (plength N)))).
set (w_op := cmk_op bb).
assert (op_spec: znz_spec w_op).
unfold bb, w_op; apply cmk_spec; auto.
assert (F0: N < DoubleType.base (znz_digits w_op)).
  apply Zlt_le_trans with (1 := plength_correct N).
  unfold w_op, DoubleType.base.
  rewrite cmk_op_digits.
  apply Zpower_le_monotone; split; auto with zarith.
  generalize (get_height_correct 31 (plength N)); unfold bb.
  set (p := plength N).
  replace (Z_of_nat (pred (nat_of_P (get_height 31 p)))) with
       ((Zpos (get_height 31 p) - 1) ); auto with zarith.
  rewrite pred_of_minus; rewrite inj_minus1; auto with zarith.
  rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith.
  generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith.
assert (F1: znz_to_Z w_op (znz_of_Z w_op N) = N).
rewrite znz_of_Z_correct; auto with zarith.
assert (F2: 1 < znz_to_Z w_op (znz_of_Z w_op N)).
rewrite F1; auto with zarith.
assert (F3: 0 < znz_to_Z w_op (znz_of_Z w_op N)); auto with zarith.
assert (F4: znz_to_Z w_op (znz_of_Z w_op a) = a).
rewrite znz_of_Z_correct; auto with zarith.
assert (F5: znz_to_Z w_op (znz_of_Z w_op 1) = 1).
rewrite znz_of_Z_correct; auto with zarith.
assert (F6: N - 1 = (R1 * mkProd_pred dec)%positive * mkProd' dec).
rewrite Zpos_mult.
rewrite <- Zmult_assoc; rewrite mkProd_pred_mkProd; auto with zarith.
simpl in H1; rewrite Zpos_mult in H1; rewrite <- H1; rewrite Ppred_Zminus;
  auto with zarith.
assert (m_spec: mod_spec w_op (znz_of_Z w_op N)
                  (make_mod_op w_op (znz_of_Z w_op N))).
apply make_mod_spec; auto with zarith.
match goal with |- context[all_pow_mod ?x ?y ?z ?t ?u] =>
  generalize (fst_all_pow_mod x w_op op_spec _ F3 _ m_spec
               u (znz_of_Z w_op a) (R1*mkProd_pred dec) z t);
  generalize (snd_all_pow_mod x w_op op_spec _ F3 _ m_spec u z t);
  fold bb w_op;
  case (all_pow_mod x y z t u); simpl fst; simpl snd
end.
intros prod aNm1; intros H5 H6.
case_eq (znz_to_Z w_op aNm1).
intros; discriminate.
2: intros; discriminate.
intros p; case p; clear p.
intros; discriminate.
intros; discriminate.
intros If6.
case_eq (znz_to_Z w_op (znz_gcd w_op prod (znz_of_Z w_op N))).
intros; discriminate.
2: intros; discriminate.
intros p; case p; clear p.
intros; discriminate.
intros; discriminate.
intros If7.
match goal with |- context[if ?x then _ else _] =>
  case_eq x; intros If8; auto
end.
2: intros; discriminate.
intros If9.
match goal with H: (?X ?< ?Y) = true |- _ =>
  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
end.
assert (U1: N - 1 = mkProd dec * R1).
rewrite <- Ppred_Zminus in H1; auto with zarith.
rewrite H1; simpl.
repeat rewrite Zpos_mult; auto with zarith.
assert (HH:Z_of_N s = R1 / (2 * mkProd dec) /\ Zpos r =  R1 mod (2 * mkProd dec)).
apply mod_unique with (2 * mkProd dec);auto with zarith.
apply Z_mod_lt; auto with zarith.
rewrite <- Z_div_mod_eq; auto with zarith.
rewrite H3.
rewrite (Zpos_xO (mkProd dec)).
simpl Z_of_N; ring.
case HH; clear HH; intros HH1 HH2.
apply PocklingtonExtra with (F1:=mkProd dec) (R1:=R1) (m:=1);
  auto with zmisc zarith.
case (Zle_lt_or_eq 1 (mkProd dec)); auto with zarith.
simpl in H2; auto with zarith.
intros HH; contradict If3; rewrite <- HH.
apply Zodd_not_Zeven; red; auto.
intros p; case p; clear p.
intros HH; contradict HH.
apply not_prime_0.
2: intros p (V1, _); contradict V1; apply Zle_not_lt; red; simpl; intros;
     discriminate.
intros p Hprime Hdec; exists (Zpos a);repeat split; auto with zarith.
apply trans_equal with (2 := If6).
rewrite H5.
rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith.
rewrite F1.
rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
rewrite F1; rewrite F4.
rewrite <- Zpower_mod; auto with zarith.
rewrite <- Zpower_mult; auto with zarith.
rewrite mkProd_pred_mkProd; auto with zarith.
rewrite U1; rewrite Zmult_comm.
rewrite Zpower_mult; auto with zarith.
rewrite <- Zpower_mod; auto with zarith.
rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith.
rewrite Zmod_small; auto with zarith.
rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
match goal with |- context[?X mod ?Y] =>
  case (Z_mod_lt X Y); auto with zarith
end.
rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith.
rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith.
match goal with |- context[?X mod ?Y] =>
  case (Z_mod_lt X Y); auto with zarith
end.
rewrite Zmod_small; auto with zarith.
rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
match goal with |- context[?X mod ?Y] =>
  case (Z_mod_lt X Y); auto with zarith
end.
rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith.
match type of H6 with _ -> _ -> ?X =>
  assert (tmp: X); [apply H6 | clear H6; rename tmp into H6];
  auto with zarith
end.
rewrite F1.
rewrite F5; rewrite Zmod_small; auto with zarith.
rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith.
repeat (rewrite F1 || rewrite F4).
rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
repeat (rewrite F1 || rewrite F4).
rewrite Zpos_mult; rewrite <- Zpower_mod; auto with zarith.
rewrite Zpower_mult; auto with zarith.
repeat (rewrite F1 || rewrite F4).
rewrite Zmod_small; auto with zarith.
rewrite Zmod_small; auto with zarith.
rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
match goal with |- context[?X mod ?Y] =>
  case (Z_mod_lt X Y); auto with zarith
end.
repeat (rewrite F1 || rewrite F4).
rewrite Zmod_small; auto with zarith.
rewrite F5 in H6; rewrite F1 in H6; rewrite F4 in H6.
case in_mkProd_prime_div_in with (3 := Hdec); auto.
intros p1 Hp1.
rewrite <- F6 in H6.
apply Zis_gcd_gcd; auto with zarith.
change (rel_prime (a ^ ((N - 1) / p) - 1) N).
match type of H6 with _ = ?X mod _ =>
  apply rel_prime_div with (p := X); auto with zarith
end.
apply rel_prime_mod_rev; auto with zarith.
red.
pattern 1 at 4; rewrite <- If7; rewrite <- H6.
pattern N at 2; rewrite <- F1.
apply spec_gcd; auto with zarith.
assert (foldtmp: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a b,
  In b l -> (forall x, P (f x b)) ->
  (forall x y, P x -> P (f x y)) ->
  P (fold_left f l a)).
assert (foldtmp0: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a,
  P a ->
  (forall x y, P x -> P (f x y)) ->
  P (fold_left f l a)).
intros A B f P l; elim l; simpl; auto.
intros A B f P l; elim l; simpl; auto.
intros a1 b HH; case HH.
intros a1 l1 Rec a2 b [V|V] V1 V2; subst; auto.
apply foldtmp0; auto.
apply Rec with (b := b); auto with zarith.
match goal with |- context [fold_left ?f _ _] =>
 apply (foldtmp _ _ f (fun k => (a ^ ((N - 1) / p) - 1 | k)))
   with (b := (p, p1)); auto with zarith
end.
rewrite <- HH2.
clear F0; match goal with H: ?X < ?Y |- ?X < ?Z =>
 replace Z with Y; auto
end.
repeat (rewrite Zpos_plus || rewrite Zpos_mult || rewrite times_Zmult).
rewrite Zpos_xO; ring.
rewrite <- HH1; rewrite <- HH2.
apply check_s_r_correct with sqrt; auto.
Qed.

(* Simple version of pocklington for primo *)
Definition test_spock N a dec :=
  if (2 ?< N) then
    let Nm1 := Ppred N in
    let F1 := mkProd dec in
    match (Nm1 / F1)%P with
    | (Npos R1, N0) =>
          if (1 ?< a) then
            if (a ?< N) then
              if (N ?< F1 * F1) then
              let op := cmk_op (pred (nat_of_P (get_height 31 (plength N)))) in
              let wN := znz_of_Z op (Zpos N) in
              let wa := znz_of_Z op (Zpos a) in
              let w1 := znz_of_Z op 1 in
              let mod_op := make_mod_op op wN in
              let pow := mod_op.(power_mod) in
              let ttimes := mod_op.(mul_mod) in
              let pred:= mod_op.(pred_mod) in
              let gcd:= op.(znz_gcd) in
              let A := pow_mod_pred _ mod_op (pow wa R1) dec in
              match all_pow_mod _ mod_op w1 A dec with
              | (p, aNm1) =>
                match znz_to_Z op aNm1 with
                  (Zpos xH) =>
                   match znz_to_Z op (gcd p wN) with
                   (Zpos xH) => true
                   | _ => false
                   end
                 | _ => false
                end
              end else false
           else false
         else false
    | _=> false
    end
  else false.

Lemma test_spock_correct : forall N a dec,
   (forall k, In k dec -> prime (Zpos (fst k))) ->
   test_spock N a dec = true ->
   prime N.
unfold test_spock;intros N a dec H.
match goal with |- context[if ?x then _ else _] =>
  case_eq x; intros If1; auto
end.
2: intros; discriminate.
match goal with H: (?X ?< ?Y) = true |- _ =>
  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
end.
generalize (div_eucl_spec (Ppred N) (mkProd dec));
 destruct ((Ppred N) / (mkProd dec))%P as (R1,n).
simpl fst; simpl snd; intros (H1, H2).
destruct R1 as [|R1].
intros; discriminate.
destruct n.
2: intros; discriminate.
match goal with |- context[if ?x then _ else _] =>
  case_eq x; intros If2; auto
end.
match goal with H: (?X ?< ?Y) = true |- _ =>
  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
end.
2: intros; discriminate.
(*
set (bb := pred (nat_of_P (get_height 31 (plength N)))).
set (w_op := cmk_op bb).
assert (op_spec: znz_spec w_op).
unfold bb, w_op; apply cmk_spec; auto.
assert (F0: N < Basic_type.base (znz_digits w_op)).
  apply Zlt_le_trans with (1 := plength_correct N).
  unfold w_op, Basic_type.base.
  rewrite cmk_op_digits.
  apply Zpower_le_monotone; split; auto with zarith.
  generalize (get_height_correct 31 (plength N)); unfold bb.
  set (p := plength N).
  replace (Z_of_nat (pred (nat_of_P (get_height 31 p)))) with
       ((Zpos (get_height 31 p) - 1) ); auto with zarith.
  rewrite pred_of_minus; rewrite inj_minus1; auto with zarith.
  rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith.
  generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith.
*)
set (bb := pred (nat_of_P (get_height 31 (plength N)))).
set (w_op := cmk_op bb).
assert (op_spec: znz_spec w_op).
unfold bb, w_op; apply cmk_spec; auto.
match goal with |- context[if ?x then _ else _] =>
  case_eq x; intros If3; auto
end.
match goal with H: (?X ?< ?Y) = true |- _ =>
  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
end.
match goal with |- context[if ?x then _ else _] =>
  case_eq x; intros If4; auto
end.
match goal with H: (?X ?< ?Y) = true |- _ =>
  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
end.
assert (F0: N < DoubleType.base (znz_digits w_op)).
  apply Zlt_le_trans with (1 := plength_correct N).
  unfold w_op, DoubleType.base.
  rewrite cmk_op_digits.
  apply Zpower_le_monotone; split; auto with zarith.
  generalize (get_height_correct 31 (plength N)); unfold bb.
  set (p := plength N).
  replace (Z_of_nat (pred (nat_of_P (get_height 31 p)))) with
       ((Zpos (get_height 31 p) - 1) ); auto with zarith.
  rewrite pred_of_minus; rewrite inj_minus1; auto with zarith.
  rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith.
  generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith.
assert (F1: znz_to_Z w_op (znz_of_Z w_op N) = N).
rewrite znz_of_Z_correct; auto with zarith.
assert (F2: 1 < znz_to_Z w_op (znz_of_Z w_op N)).
rewrite F1; auto with zarith.
assert (F3: 0 < znz_to_Z w_op (znz_of_Z w_op N)); auto with zarith.
assert (F4: znz_to_Z w_op (znz_of_Z w_op a) = a).
rewrite znz_of_Z_correct; auto with zarith.
assert (F5: znz_to_Z w_op (znz_of_Z w_op 1) = 1).
rewrite znz_of_Z_correct; auto with zarith.
assert (F6: N - 1 = (R1 * mkProd_pred dec)%positive * mkProd' dec).
rewrite Zpos_mult.
rewrite <- Zmult_assoc; rewrite mkProd_pred_mkProd; auto with zarith.
simpl in H1; rewrite Zpos_mult in H1; rewrite <- H1; rewrite Ppred_Zminus;
  auto with zarith.
assert (m_spec: mod_spec w_op (znz_of_Z w_op N)
                  (make_mod_op w_op (znz_of_Z w_op N))).
apply make_mod_spec; auto with zarith.
match goal with |- context[all_pow_mod ?x ?y ?z ?t ?u] =>
  generalize (fst_all_pow_mod x w_op op_spec _ F3 _ m_spec
               u (znz_of_Z w_op a) (R1*mkProd_pred dec) z t);
  generalize (snd_all_pow_mod x w_op op_spec _ F3 _ m_spec u z t);
  fold bb w_op;
  case (all_pow_mod x y z t u); simpl fst; simpl snd
end.
2: intros; discriminate.
intros prod aNm1; intros H5 H6.
case_eq (znz_to_Z w_op aNm1).
intros; discriminate.
2: intros; discriminate.
intros p; case p; clear p.
intros; discriminate.
intros; discriminate.
intros If5.
case_eq (znz_to_Z w_op (znz_gcd w_op prod (znz_of_Z w_op N))).
intros; discriminate.
2: intros; discriminate.
intros p; case p; clear p.
intros; discriminate.
intros; discriminate.
intros If6 _.
assert (U1: N - 1 = mkProd dec * R1).
rewrite <- Ppred_Zminus in H1; auto with zarith.
rewrite H1; simpl.
repeat rewrite Zpos_mult; auto with zarith.
apply PocklingtonCorollary1 with (F1:=mkProd dec) (R1:=R1);
  auto with zmisc zarith.
case (Zle_lt_or_eq 1 (mkProd dec)); auto with zarith.
simpl in H2; auto with zarith.
intros HH; contradict If4; rewrite Zpos_mult_morphism;
  rewrite <- HH.
apply Zle_not_lt; auto with zarith.
intros p; case p; clear p.
intros HH; contradict HH.
apply not_prime_0.
2: intros p (V1, _); contradict V1; apply Zle_not_lt; red; simpl; intros;
     discriminate.
intros p Hprime Hdec; exists (Zpos a);repeat split; auto with zarith.
apply trans_equal with (2 := If5).
rewrite H5.
rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith.
rewrite F1.
rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
rewrite F1; rewrite F4.
rewrite <- Zpower_mod; auto with zarith.
rewrite <- Zpower_mult; auto with zarith.
rewrite mkProd_pred_mkProd; auto with zarith.
rewrite U1; rewrite Zmult_comm.
rewrite Zpower_mult; auto with zarith.
rewrite <- Zpower_mod; auto with zarith.
rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith.
rewrite Zmod_small; auto with zarith.
rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
match goal with |- context[?X mod ?Y] =>
  case (Z_mod_lt X Y); auto with zarith
end.
rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith.
rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith.
match goal with |- context[?X mod ?Y] =>
  case (Z_mod_lt X Y); auto with zarith
end.
rewrite Zmod_small; auto with zarith.
rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
match goal with |- context[?X mod ?Y] =>
  case (Z_mod_lt X Y); auto with zarith
end.
rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith.
match type of H6 with _ -> _ -> ?X =>
  assert (tmp: X); [apply H6 | clear H6; rename tmp into H6];
  auto with zarith
end.
rewrite F1.
rewrite F5; rewrite Zmod_small; auto with zarith.
rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith.
repeat (rewrite F1 || rewrite F4).
rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
repeat (rewrite F1 || rewrite F4).
rewrite Zpos_mult; rewrite <- Zpower_mod; auto with zarith.
rewrite Zpower_mult; auto with zarith.
repeat (rewrite F1 || rewrite F4).
rewrite Zmod_small; auto with zarith.
rewrite Zmod_small; auto with zarith.
rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
match goal with |- context[?X mod ?Y] =>
  case (Z_mod_lt X Y); auto with zarith
end.
repeat (rewrite F1 || rewrite F4).
rewrite Zmod_small; auto with zarith.
rewrite F5 in H6; rewrite F1 in H6; rewrite F4 in H6.
case in_mkProd_prime_div_in with (3 := Hdec); auto.
intros p1 Hp1.
rewrite <- F6 in H6.
apply Zis_gcd_gcd; auto with zarith.
change (rel_prime (a ^ ((N - 1) / p) - 1) N).
match type of H6 with _ = ?X mod _ =>
  apply rel_prime_div with (p := X); auto with zarith
end.
apply rel_prime_mod_rev; auto with zarith.
red.
pattern 1 at 4; rewrite <- If6; rewrite <- H6.
pattern N at 2; rewrite <- F1.
apply spec_gcd; auto with zarith.
assert (foldtmp: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a b,
  In b l -> (forall x, P (f x b)) ->
  (forall x y, P x -> P (f x y)) ->
  P (fold_left f l a)).
assert (foldtmp0: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a,
  P a ->
  (forall x y, P x -> P (f x y)) ->
  P (fold_left f l a)).
intros A B f P l; elim l; simpl; auto.
intros A B f P l; elim l; simpl; auto.
intros a1 b HH; case HH.
intros a1 l1 Rec a2 b [V|V] V1 V2; subst; auto.
apply foldtmp0; auto.
apply Rec with (b := b); auto with zarith.
match goal with |- context [fold_left ?f _ _] =>
 apply (foldtmp _ _ f (fun k => (a ^ ((N - 1) / p) - 1 | k)))
   with (b := (p, p1)); auto with zarith
end.
intros; discriminate.
Qed.

Fixpoint test_Certif (lc : Certif) : bool :=
  match lc with
  | nil => true
  | (Proof_certif _ _) :: lc => test_Certif lc
  | (Lucas_certif n p) :: lc =>
     let xx := test_Certif lc in
     if xx then
     let yy := gt2 p in
     if yy then
       match p with
         Zpos p1 =>
           let zz := Mp p in
           match zz with
          | Zpos n' =>
             if (n ?= n')%P then
               let tt :=  lucas p1 in
               match tt with
               | Z0 => true
               | _ => false
               end
             else false
           | _ => false
           end
         | _ => false
       end
    else false
    else false
  | (Pock_certif n a dec sqrt) :: lc =>
    let xx := test_pock n a dec sqrt in
    if xx then
      let yy := all_in lc dec in
      (if yy then test_Certif lc else false)
    else false
  | (SPock_certif n a dec) :: lc =>
    let xx :=test_spock n a dec in
    if xx then
      let yy := all_in lc dec in
      (if yy then test_Certif lc else false)
    else false
  | (Ell_certif n ss l a b x y) :: lc =>
    let xx := ell_test n ss l a b x y in
    if xx then
     let yy :=  all_in lc l in
     if yy then test_Certif lc else false
    else false
  end.

Lemma test_Certif_In_Prime :
  forall lc, test_Certif lc = true ->
   forall c, In c lc -> prime (nprim c).
intros lc; elim lc; simpl; auto.
intros _ c H; case H.
intros a; case a; simpl; clear a lc.
intros N p l Rec H c [H1 | H1]; subst; auto with arith.
intros n p l; case (test_Certif l); auto with zarith.
2: intros; discriminate.
intros H H1 c [H2 | H2]; subst; auto with arith.
simpl nprim.
generalize H1; clear H1.
case_eq (gt2 p).
2: intros; discriminate.
case p; clear p; try (intros; discriminate; fail).
unfold gt2; intros p H1.
match goal with H: (?X ?< ?Y) = true |- _ =>
  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
end.
unfold Mp; case_eq (2 ^ p  -1); try (intros; discriminate; fail).
intros p1 Hp1.
case_eq (n ?= p1)%P; try rewrite <- Hp1.
2: intros; discriminate.
intros H2.
match goal with H: (?X ?= ?Y)%P = true |- _ =>
  generalize (is_eq_eq _ _ H); clear H; intros H
end.
generalize (lucas_prime H1); rewrite Hp1; rewrite <- H2.
case (lucas p); try (intros; discriminate; fail); auto.
intros N a d p l H.
generalize (test_pock_correct N a d p).
case (test_pock N a d p); auto.
2: intros; discriminate.
generalize (all_in_In l d).
case (all_in l d).
2: intros; discriminate.
intros H1 H2 H3 c [H4 | H4]; subst; simpl; auto.
apply H2; auto.
intros k Hk.
case H1 with (2 := Hk); auto.
intros x (Hx1, Hx2); rewrite Hx2; auto.
intros N a d l H.
generalize (test_spock_correct N a d).
case test_spock; auto.
2: intros; discriminate.
generalize (all_in_In l d).
case (all_in l d).
2: intros; discriminate.
intros H1 H2 H3 c [H4 | H4]; subst; simpl; auto.
apply H2; auto.
intros k Hk.
case H1 with (2 := Hk); auto.
intros x (Hx1, Hx2); rewrite Hx2; auto.
intros N S l A B x y l1.
generalize (all_in_In l1 l).
generalize (ell_test_correct N S l A B x y).
case ell_test.
case all_in; auto.
intros H1 H2 H3 H4 c [H5 | H5]; try subst c; simpl; auto.
apply H1.
intros p Hp; case (H2 (refl_equal true) p); auto.
intros x1 (Hx1, Hx2); rewrite Hx2; auto.
intros; discriminate.
intros; discriminate.
Qed.

Lemma Pocklington_refl :
  forall c lc, test_Certif (c::lc) = true -> prime (nprim c).
Proof.
 intros c lc Heq;apply test_Certif_In_Prime with (c::lc);trivial;simpl;auto.
Qed.

author: EasyCrypt

repo: certicrypt

save_path: github-repos/coq/EasyCrypt-certicrypt


text:
Require Import String.
Require Import Coq.Numbers.Natural.Peano.NPeano.
Require Import Coq.Strings.Ascii.

Definition natToDigit (n : nat) : ascii :=
  match n with
  | 0 => "0"
  | 1 => "1"
  | 2 => "2"
  | 3 => "3"
  | 4 => "4"
  | 5 => "5"
  | 6 => "6"
  | 7 => "7"
  | 8 => "8"
  | _ => "9"
  end.

Fixpoint natToString' (time n : nat) (acc : string) : string :=
  let acc' := String (natToDigit (n mod 10)) acc in
  match time with
  | 0 => acc'
  | S time' =>
    match n / 10 with
    | 0 => acc'
    | n' => natToString' time' n' acc'
    end
  end.

Definition natToString (n : nat) : string :=
  natToString' n n "".

Definition boolToString (b: bool) : string :=
  if b then "true" else "false".

author: atlanmod

repo: coqtl

save_path: github-repos/coq/atlanmod-coqtl


text:
(*
  Problem(s):
    Weak call-by-name leftmost outermost normalization (wCBN)
    Weak call-by-name leftmost outermost normalization for closed terms (wCBNclosed)

  Literature:
    [1] Plotkin, Gordon.
    "Call-by-name, call-by-value and the λ-calculus."
    Theoretical computer science 1.2 (1975): 125-159.
*)

Require Undecidability.L.L.
Import L (term, var, app, lam).

Require Import Relation_Operators.

(* function composition *)
Definition funcomp {X Y Z} (g : Y -> Z) (f : X -> Y) :=
  fun x => g (f x).

Arguments funcomp {X Y Z} (g f) /.

(* stream cons *)
Definition scons {X: Type} (x : X) (xi : nat -> X) :=
  fun n => match n with | 0 => x | S n => xi n end.

(* parallel term renaming *)
Fixpoint ren (xi : nat -> nat) (t : term) : term  :=
  match t with
  | var x => var (xi x)
  | app s t => app (ren xi s) (ren xi t)
  | lam t => lam (ren (scons 0 (funcomp S xi)) t)
  end.

(* parallel term substitution *)
Fixpoint subst (sigma: nat -> term) (s: term) : term :=
  match s with
  | var n => sigma n
  | app s t => app (subst sigma s) (subst sigma t)
  | lam s => lam (subst (scons (var 0) (funcomp (ren S) sigma)) s)
  end.

(* left-most outer-most call-by-name reduction *)
Inductive step : term -> term -> Prop :=
  | stepLam s t    : step (app (lam s) t) (subst (scons t var) s)
  | stepApp s s' t : step s s' -> step (app s t) (app s' t).

(* weak call-by-name leftmost outermost normalization *)
Definition wCBN : term -> Prop :=
  fun s => exists t, clos_refl_trans term step s t /\ forall u, not (step t u).

(* weak call-by-name leftmost outermost normalization of closed terms *)
Definition wCBNclosed : { s : term | forall sigma, subst sigma s = s } -> Prop :=
  fun '(exist _ s _) => exists t, clos_refl_trans term step s (lam t).

author: uds-psl

repo: coq-library-undecidability


text:
Require Import Arith List.
Require Import Cpdt.CpdtTactics.
Set Implicit Arguments.
Set Asymmetric Patterns.

Section tree.
  Variable A : Type.

  Inductive tree : Type :=
  | Leaf : A -> tree
  | Node : tree -> tree -> tree.
End tree.

(* Inductive *)

Section htree.
  Variable A : Type.
  Variable B : A -> Type.

  Inductive htree : tree A -> Type :=
  | HLeaf : forall (x : A), B x -> htree (Leaf x)
  | HNode : forall l r, htree l -> htree r -> htree (Node l r).

  Variable elm : A.

  Inductive path : tree A -> Type :=
  | Stop : path (Leaf elm)
  | Left : forall l r, path l -> path (Node l r)
  | Right : forall l r, path r -> path (Node l r).

  Fixpoint tget t (ht : htree t) : path t -> B elm :=
    match ht with
    | HLeaf _ b => fun p =>
        match p in path t' return (match t' with
                                   | Leaf x => B x -> B elm
                                   | Node _ _ => unit
                                   end) with
        | Stop => fun b => b
        | Left _ _ _ => tt
        | Right _ _ _ => tt
        end b
    | HNode _ _ hl hr => fun p =>
        match p in path t' return (match t' with
                                   | Leaf _ => unit
                                   | Node l r => (path l -> B elm) -> (path r -> B elm) -> B elm
                                   end) with
        | Stop => tt
        | Left _ _ p' => fun tget_l _ => tget_l p'
        | Right _ _ p' => fun _ tget_r => tget_r p'
        end (tget hl) (tget hr)
    end.
End htree.

Implicit Arguments HLeaf [A B x].
Implicit Arguments HNode [A B l r].
Implicit Arguments Stop [A elm].
Implicit Arguments Left [A elm l r].
Implicit Arguments Right [A elm l r].

Example someTypes : tree Set :=
  Node (Node (Leaf nat) (Leaf unit)) (Leaf bool).
Example someValues : htree (fun T : Set => T) someTypes :=
  HNode (HNode (HLeaf 42) (HLeaf tt)) (HLeaf true).

Eval simpl in tget someValues (Right Stop).
Eval simpl in tget someValues (Left (Right Stop)).
Eval simpl in tget someValues (Left (Left Stop)).

Section htmap2.
  Variable A : Type.
  Variables B1 B2 C : A -> Type.
  Variable f : forall x, B1 x -> B2 x -> C x.

  Fixpoint htmap2 t (ht1 : htree B1 t) (ht2 : htree B2 t) : htree C t :=
    match ht1 in htree _ t return htree _ t -> htree _ t with
    | HLeaf x b1 => fun ht2 =>
      match ht2
            in htree _ t'
            return
            match t' with
            | Leaf x' => B1 x' -> htree _ t'
            | Node _ _ => B1 x -> unit
            end
      with
      | HLeaf _ b2 => fun b1 => HLeaf (f b1 b2)
      | HNode _ _ _ _ => fun _ => tt
      end b1
    | HNode l r hl1 hr1 => fun ht2 =>
      match ht2
            in htree _ t'
            return
            match t' with
            | Leaf _ =>
              (htree B2 l -> htree C l) ->
              (htree B2 r -> htree C r) ->
              unit
            | Node l r =>
              (htree B2 l -> htree C l) ->
              (htree B2 r -> htree C r) ->
              htree C (Node l r)
            end
      with
      | HLeaf _ _ => fun _ _ => tt
      | HNode _ _ hl2 hr2 =>
        fun htmap2_l htmap2_r => HNode (htmap2_l hl2) (htmap2_r hr2)
      end (htmap2 hl1) (htmap2 hr1)
    end ht2.
End htmap2.

(* Recursive *)

Section fhtree.
  Variable A : Type.
  Variable B : A -> Type.

  Fixpoint fhtree (t : tree A) : Type :=
    match t with
    | Leaf x => B x
    | Node l r => fhtree l * fhtree r
    end%type.

  Variable elm : A.

  Fixpoint fpath (t : tree A) : Type :=
    match t with
    | Leaf x => x = elm
    | Node l r => fpath l + fpath r
    end%type.

  Fixpoint ftget (t : tree A) : fhtree t -> fpath t -> B elm :=
    match t with
    | Leaf x => fun b p =>
      match p with eq_refl => b end
    | Node l r => fun b p =>
      match p with
      | inl p' => ftget l (fst b) p'
      | inr p' => ftget r (snd b) p'
      end
    end.
End fhtree.

Section fhtmap2.
  Variable A : Type.
  Variables B1 B2 C : A -> Type.
  Variable f : forall x, B1 x -> B2 x -> C x.

  Fixpoint fhtmap2 (t : tree A) : fhtree B1 t -> fhtree B2 t -> fhtree C t :=
    match t with
    | Leaf x => fun b1 b2 => f b1 b2
    | Node l r => fun ht1 ht2 =>
      (fhtmap2 l (fst ht1) (fst ht2), fhtmap2 r (snd ht1) (snd ht2))
    end.
End fhtmap2.

(* Index Function *)

Section fhtree'.
  Variable A : Type.
  Variable B : A -> Type.

  Definition fhtree' (t : tree A) := forall elm, fpath elm t -> B elm.
  Variable elm : A.

  Definition ftget' (t : tree A) : fhtree' t -> fpath elm t -> B elm :=
    fun f p => f elm p.
End fhtree'.

Section fhtmap2'.
  Variable A : Type.
  Variables B1 B2 C : A -> Type.
  Variable f : forall x, B1 x -> B2 x -> C x.

  Definition fhtmap2' (t : tree A) : fhtree' B1 t -> fhtree' B2 t -> fhtree' C t :=
    fun f1 f2 => fun elm p => f (f1 elm p) (f2 elm p).
End fhtmap2'.

author: manzyuk

repo: cpdt-exercises

save_path: github-repos/coq/manzyuk-cpdt-exercises


text:
From Undecidability.L Require Import Tactics.Computable Lproc Lbeta ComputableTime mixedTactics.
Import L_Notations.

(* *** Lrewrite: simplification with correctness statements*)

(* This module simplifies L-terms by rewriting with correctness-lemmatas form the hint library Lrewrite *)

(* For Time Complexity: *)

Lemma redLe_app_helper s s' t t' u i j k:
  s >(<= i) s' -> t >(<= j) t' -> s' t' >(<=k) u -> s t >(<=i+j+k) u.
Proof.
  intros (i' & ? & R1)  (j' & ? & R2)  (k' & ? & R3).
  exists ((i'+j')+k'). split. lia. apply pow_trans with (t:=s' t').
  apply pow_trans with (t:=s' t).
  now apply pow_step_congL.
  now apply pow_step_congR. eauto.
Qed.

Lemma pow_app_helper s s' t t' u:
  s >* s' -> t >* t' -> s' t' >* u -> s t >* u.
Proof.
  now intros -> -> -> .
Qed.

Lemma LrewriteTime_helper s s' t i :
  s' = s -> s >(<= i) t -> s' >(<= i) t.
Proof.
  intros;now subst.
Qed.

Lemma Lrewrite_helper s s' t :
  s' = s -> s >* t -> s' >* t.
Proof.
  intros;now subst.
Qed.

Lemma Lrewrite_equiv_helper s s' t t' :
  s >* s' -> t >* t' -> s' == t' -> s == t.
Proof.
  intros -> ->. tauto.
Qed.

Ltac find_Lrewrite_lemma :=
  once lazymatch goal with
    | |- ?R (lam _) => fail
    | |- ?R (enc _) => fail
    | |- ?R (extT (ty:=TyB _) _) => fail
    | |- ?R (ext (ty:=TyB _) _) => fail
    | |- ?R ?s _ => has_no_evar s;solve [eauto 20 with Lrewrite nocore]
  end.

Create HintDb Lrewrite discriminated.
Hint Constants Opaque : Lrewrite.
Hint Variables Opaque : Lrewrite.

Hint Extern 0 (proc _) => solve [Lproc] : Lrewrite.
Hint Extern 0 (lambda _) => solve [Lproc] : Lrewrite.
Hint Extern 0 (closed _) => solve [Lproc] : Lrewrite.

Lemma pow_redLe_subrelation' i s t : pow step i s t -> redLe i s t.
Proof. apply pow_redLe_subrelation. Qed. (* for performance, without [subrelation] in type*)

Hint Extern 0 (_ >(<= _ ) _) => simple eapply pow_redLe_subrelation' : Lrewrite.
Hint Extern 0 (_ >* _) => simple eapply redLe_star_subrelation : Lrewrite.
Hint Extern 0 (_ >* _) => simple eapply eval_star_subrelation : Lrewrite.

(* replace int by intT if possible*)

Ltac Ltransitivity :=
  once lazymatch goal with
  | |- _ >(<= _ ) _ => refine (redLe_trans _ _);[shelve.. | | ]
  | |- _ >* _ => refine (star_trans _ _);[shelve.. | | ]
  | |- _ >(_) _ => eapply pow_add with (R:=step)
  | |- ?t => fail "not supported by Ltransitivity:" t
  end.

(* generate all goals for bottom-up-rewriting*)
Ltac Lrewrite_generateGoals :=
  once lazymatch goal with
  | |- app _ _ >(<= _ ) _ => eapply redLe_app_helper;[instantiate;Lrewrite_generateGoals..|idtac]
  | |- app _ _ >* _ => eapply pow_app_helper  ;[instantiate;Lrewrite_generateGoals..|idtac]
  | |- ?s >(<= _ ) _ => (is_evar s;fail 10000) ||idtac
  | |- ?s >* _ => (is_evar s;reflexivity) ||idtac
  end.

Ltac useFixHypo :=
  once lazymatch goal with
    |- ?s >* ?t =>
    has_no_evar s;
    let IH := fresh "IH" in
    unshelve epose (IH:=_);[|(notypeclasses refine (_:{v:term & computesExp _ _ s v}));solve [once auto with nocore]|];
    let v := constr:(projT1 IH) in
    assert (IHR := fst (projT2 IH));
    let IHInts := constr:( snd (projT2 IH)) in
    once lazymatch type of IHInts with
      computes ?ty _ ?v =>
      change v with (@ext _ ty _ (Build_computable IHInts)) in IHR;exact (proj1 IHR)
    end
  | |- ?s >(<= ?i ) ?t=>
    has_no_evar s;
    let IH := fresh "IH" in
    unshelve epose (IH:=_);[|(notypeclasses refine (_:{v:term & computesTimeExp _ _ s _ v _}));solve [once auto with nocore]|];
    (* (let t := type of IH in idtac "Used IH:" t); *)
    let v := constr:(projT1 IH) in
    assert (IHR := fst (projT2 IH));
    let IHInts := constr:( snd (projT2 IH)) in
    once lazymatch type of IHInts with
      computesTime ?ty _ ?v _=>
      change v with (@extT _ ty _ _ (Build_computableTime IHInts)) in IHR;exact (proj1 IHR)
    end
  end.

Ltac LrewriteTime_solveGoals :=
  try find_Lrewrite_lemma;
  try useFixHypo;
  once lazymatch goal with
    (* Computability: *)
  | |- @ext _ (@TyB _ _)  _ ?inted >* _ =>
    (progress rewrite (ext_is_enc);[>LrewriteTime_solveGoals..]) || Lreflexivity
  | |- app (@ext _ (_ ~> _ ) _ _) (ext _) >* _ => etransitivity;[apply extApp|LrewriteTime_solveGoals]
  | |- app (@ext _ (_ ~> _ ) _ ?ints) (@enc _ ?reg ?x) >* ?v =>
    change (app (@ext _ _ _ ints) (@ext _ _ _ (reg_is_ext reg x)) >* v);LrewriteTime_solveGoals

  (* Complexity*)
  | |- @extT _ (@TyB _ _) _ _ ?inted >(<= _ ) _ =>
    (progress rewrite (extT_is_enc);[>LrewriteTime_solveGoals..]) || Lreflexivity
  | |- app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _ => eapply redLe_trans;
    [let R := fresh "R" in
     specialize (extTApp fInts xInts) as R;
     once lazymatch type of R with
       (* As we might build n using the projection on an on-ty-fly constructed computableTime-instance, we mustavoid it to depend on the proof that the time function is correct*)
       ?s >(<= ?n) ?t => let n' := eval unfold evalTime in n in
                          change (s >(<= n') t) in R
     end; exact R
    |LrewriteTime_solveGoals]
  | |- app (@extT _ (_ ~> _ ) _ _ ?ints) (@enc _ ?reg ?x) >(<= ?k ) ?v =>
    change (app (@extT _ _ _ _ ints) (@extT _ _ _ _ (reg_is_extT reg x)) >(<= k) v);LrewriteTime_solveGoals

  (*| xInts : computes ?ty ?x ?xInt _
    |- ?R ?xInt ?res => change (R (@ext _ _ x (Build_computable xInts)) res)
                      ;reflexivity*)
  (* Correctness Lemmatas: *)

(* do nothing to debug: use idtac here!*)
  | |- _ >(<= _ ) _ => Lreflexivity (* TO DEBUG: use idtac here*)
  | |- _ >* _ => reflexivity (* TO DEBUG: use idtac here*)
  end.

Ltac Lrewrite' :=
  once lazymatch goal with
    |- ?rel ?s _ =>
    once lazymatch goal with
    | |- _ >(<=_) _ =>
      try (eapply redLe_trans;[Lrewrite_generateGoals;[>LrewriteTime_solveGoals..]|])
    | |- _ >* _ =>
      try (etransitivity;[Lrewrite_generateGoals;[>LrewriteTime_solveGoals..]|])
    end;
      once lazymatch goal with
        |- ?rel s _ => fail "No Progress (progress in indices are not currently noticed...)"
      (* don;t change evars if you did not make progress!*)
      | |- _ => idtac
      end
  | |- _ => idtac
  end.

Tactic Notation "Lrewrite_wrapper" tactic(k):=
once lazymatch goal with
| |- _ >(<= _) _ => k
| |- _ ⇓(<= _) _ => (eapply evalLe_trans;[k;Lreflexivity|])
| |- _ ⇓( _) _ => idtac "Lrewrite_prepare does not support s ⇓(k) y, only s ⇓(<=k) t)" (*try (eapply evalIn_trans;[progress Lrewrite_prepare;Lreflexivity|])*)
| |- _ >(_) _ => idtac "Lrewrite_prepare does not support s >(k) y, only s >(<=k) t)"
| |- _ >* _ => k (* Lrewrite_prepare_old *)
| |- eval _ _ => (eapply eval_helper;[k;Lreflexivity|])
| |- _ == _ => progress ((eapply Lrewrite_equiv_helper;[try (* inefficient, but needed if only one side does progress *)k;reflexivity..|]))
end.

(* does work on coq variables that are not abstactions *)
Ltac Lrewrite := Lrewrite_wrapper Lrewrite'.

Lemma Lrewrite_in_helper s t s' t' :
  s >* s' -> t >* t' -> s == t -> s' == t'.
Proof.
  intros R1 R2 E. now rewrite R1,R2 in E.
Qed.

Tactic Notation "Lrewrite" "in" hyp(_H) :=
  once lazymatch type of _H with
    | _ == _ => eapply Lrewrite_in_helper in _H; [ |try Lrewrite;reflexivity |try Lrewrite;reflexivity]
    | _ >* _ => idtac "not supported yet"
  end.

Lemma ext_rel_helper X `(H:encodable X) (x:X) (inst : computable x) (R: term -> term -> Prop) u:
  R (enc x) u -> R (@ext _ _ _ inst) u.
Proof.
  now rewrite ext_is_enc.
Qed.

Lemma extT_rel_helper X `(H:encodable X) (x:X) xT (inst : computableTime x xT) (R: term -> term -> Prop) u:
  R (enc x) u -> R (@extT _ _ _ _ inst) u.
Proof.
  now rewrite extT_is_enc.
Qed.

(* version of Lrewrite that des the beta-steps as well *)
Ltac LrewriteSimpl_old':=
  idtac;
  (* time "LrewriteSimpl'" *) (
  once lazymatch goal with
  | |- _ (@ext _ (@TyB _ ?reg) _ _) _ => eapply ext_rel_helper (* for backwards-compability, if used on term with hole*)
  | |- _ (@extT _ (@TyB _ ?reg) _ _ _) _ => eapply extT_rel_helper (* for backwards-compability, if used on term with hole*)
  | |- ?R ?s _  => has_no_evar s(* ;idtac "head" s *)
  end;
  once lazymatch goal with
  | |- ?R (L.app _ _) _ =>
    (* first reduce recursively *)
    (once lazymatch R with
     |  star step => refine (pow_app_helper _ _ _)
     | redLe _ => refine (redLe_app_helper _ _ _)
     end);[LrewriteSimpl_old';Lreflexivity..| ];

    (* then reduce here/above *)
    once lazymatch goal with
         (* beta-reduce here & recurse down again (if argument abstraction)*)
         | |- _ (L.app (lam _) ?t) _ =>
           let valt := fresh "valt" in
           assert (valt:proc t) by Lproc;
           Lbeta; (*;
           once lazymatch goal with
             |- _ (L.app (lam _) t) _ => fail "could not reduce"
           | |- _ => idtac
           end; *)
           clear valt;LrewriteSimpl_old'
         | |- _ =>

           let appTimeHelper tt:=
               (once lazymatch goal with
                | |- app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _
                  => let R := fresh "R" in
                    specialize (extTApp fInts xInts) as R;
                    once lazymatch type of R with
                      (* As we might build n using the projection on an on-ty-fly constructed computableTime-instance, we mustavoid it to depend on the proof that the time function is correct*)
                      ?s >(<= ?n) ?t => (
                        let n' := eval unfold evalTime in n in
                            change (s >(<= n') t) in R)
                    end; Ltransitivity;[exact R|]
                end) in

           (* use correctness lemmates of int here*)
           once lazymatch goal with
           | |- L.app (@ext _ (_ ~> _ ) _ _) (ext _) >* _ => Ltransitivity;[apply extApp|]
           | |- L.app (@ext _ (_ ~> _ ) _ ?ints) (@enc _ ?reg ?x) >* ?v =>
             change (app (@ext _ _ _ ints) (@ext _ _ _ (reg_is_ext reg x)) >* v);
             Ltransitivity;[apply extApp|]

           | |- L.app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _ => appTimeHelper tt
           | |- L.app (@extT _ (_ ~> _ ) _ _ ?ints) (@enc _ ?reg ?x) >(<= ?k ) ?v =>
             change (L.app (@extT _ _ _ _ ints) (@extT _ _ _ _ (reg_is_extT reg x)) >(<= k) v);appTimeHelper tt
           | |- _ => idtac

           end
         end
  | |- _ => idtac
  end;
  try repeat' (Ltransitivity;[find_Lrewrite_lemma|LrewriteSimpl_old']);
  try (once (Ltransitivity;[useFixHypo|]));
  (* clean up goal*)
  once lazymatch goal with
  | |- _ (@ext _ (@TyB _ ?reg) _ _) _ => eapply ext_rel_helper
  | |- _ (@extT _ (@TyB _ ?reg) _ _ _) _ => eapply extT_rel_helper
  | |- _ => idtac
  end).

Lemma LrewriteTime_helper_index:
forall [s t : term] [i i' : nat], i = i' -> s >(<=i) t -> s >(<=i') t.
Proof. intros. now subst. Qed.

Lemma redLe_app_helperL s s' t u i j:
s >(<= i) s' -> app s' t >(<=j) u -> app s t >(<=i+j) u.
Proof. intros ? H'. eapply redLe_app_helper in H'. 2:eassumption. 2:Lreflexivity. now rewrite Nat.add_0_r in H'. Qed.

Lemma redLe_app_helperR s t t' u i j:
t >(<= i) t' -> app s t' >(<=j) u -> app s t >(<=i+j) u.
Proof. intros ? H'. eapply redLe_app_helper in H'. 3:eassumption. 2:Lreflexivity. eassumption. Qed.

Lemma pow_app_helperL s s' t u:
s >* s' -> app s' t >* u -> app s t >* u.
Proof. now intros -> -> . Qed.

Lemma pow_app_helperR s t t' u:
t >* t' -> app s t' >* u -> app s t >* u.
Proof. now intros -> -> . Qed.

Ltac LrewriteSimpl_appL R:=
  lazymatch R with
  | star step => refine (pow_app_helperL _ _)
  | redLe _ => refine (redLe_app_helperL _ _)
  end.

Ltac LrewriteSimpl_appR R:=
lazymatch R with
| star step => refine (pow_app_helperR _ _)
| redLe _ => refine (redLe_app_helperR _ _)
end.

Ltac appTimeHelper tt:=
 (* As we might build n using the projection on an on-ty-fly constructed computableTime-instance, we mustavoid it to depend on the proof that the time function is correct*)
  (once lazymatch goal with
  | |- app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _
    => Ltransitivity;[refine (LrewriteTime_helper_index _ (extTApp fInts xInts));[unfold evalTime;reflexivity]| ]
    end ).

Ltac isValue s:=
  lazymatch s with
  | lam _ => idtac
  | app _ _ => fail
  | @ext _ _ _ _ => idtac
  | @extT _ _ _ _ _ => idtac
  | @enc _ _ _ => idtac
  | I => idtac
  | ?P => tryif (is_var P;lazymatch eval unfold P in P with rho _ => idtac end) then idtac
          else
          lazymatch goal with
          | H : proc s |- _  => idtac
          | H : lambda s |- _ => idtac
          | _ => (* idtac "noFastValue, default to true" s; *)idtac
          end
  end.

(* version of Lrewrite that des the beta-steps as well *)
(* clears the flag iff head is not applied to values *)
Ltac LrewriteSimpl'' canReduceFlag :=
  idtac;
  (* time "LrewriteSimpl'" *)
  once lazymatch goal with
  | |- _ (@ext _ (@TyB _ ?reg) _ _) _ => refine (ext_rel_helper _ _) (* for backwards-compability, if used on term with hole*)
  | |- _ (@extT _ (@TyB _ ?reg) _ _ _) _ => refine (extT_rel_helper _ _) (* for backwards-compability, if used on term with hole*)
  | |- ?R ?s _  => has_no_evar s;(* idtac "recurse to" s; *)

  repeat' (idtac;
    lazymatch goal with
    | |- _ (lam _) _ => fail
    | |- _ (enc _) _ => fail

    (* use correctness lemmatas of int here*)
    | |- L.app (@ext _ (_ ~> _ ) _ _) (ext _) >* _ => Ltransitivity;[apply extApp|]
    | |- L.app (@ext _ (_ ~> _ ) _ ?ints) (@enc _ ?reg ?x) >* ?v =>
      change (app (@ext _ _ _ ints) (@ext _ _ _ (reg_is_ext reg x)) >* v);
      Ltransitivity;[refine (extApp _ _)|]
    | |- L.app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _ => appTimeHelper tt
    | |- L.app (@extT _ (_ ~> _ ) _ _ ?ints) (@enc _ ?reg ?x) >(<= ?k ) ?v =>
      change (L.app (@extT _ _ _ _ ints) (@extT _ _ _ _ (reg_is_extT reg x)) >(<= k) v);appTimeHelper tt

    (* clean up goal *)
    | |- _ (@ext _ (@TyB _ ?reg) _ _) _ => refine (ext_rel_helper _ _)
    | |- _ (@extT _ (@TyB _ ?reg) _ _ _) _ => refine (extT_rel_helper _ _)

      (* last reduce recursively, and then try to apply rewrite lemmas o Lbeta *)
    | |- ?R (L.app _ _) _ =>
      (* idtac "at app0"; *)
      let progressFlag := fresh in
      let recCanReduceFlag := fresh  in
      let tmp := fresh in
      assert (progressFlag:=tt);
      assert (tmp:=tt);
      assert (recCanReduceFlag:=tt);
      try (LrewriteSimpl_appR R;[solve [LrewriteSimpl'' tmp;Lreflexivity]|(* idtac"didR"; *)try clear progressFlag]);
      try clear tmp; (*we don't care for RHS*)
      try (LrewriteSimpl_appL R;[solve [LrewriteSimpl'' canReduceFlag;Lreflexivity]|(* idtac"didL"; *)try clear progressFlag]);
      (* idtac "at app"; *)
      lazymatch goal with
      | |- ?R (L.app ?s ?t) _ =>
        (* idtac "still app" s t; *)
        let maybeBeta _ := lazymatch s with lam _ => Lbeta end in
        try (maybeBeta ();try clear progressFlag);
        tryif (tryif is_var recCanReduceFlag then isValue t else fail)
          then
            try (
              Ltransitivity;[solve [find_Lrewrite_lemma|useFixHypo]|];
              try clear progressFlag (* we did something *);

              (* We mus re-evaluate if we produce an assumption where s rewrite could apply*)
              try (clear canReduceFlag;pose (canReduceFlag:=tt))
            )
          else clear canReduceFlag
      end;
      (* fail if no progress *)
      tryif is_var progressFlag then (* lazymatch goal with |- ?H => idtac "leaving behind" H end; *)fail else idtac
(*     | |- ?H => fail 1000 "unexpected goal" H  *)
    | |- ?H => (* idtac "fallback" H; *)Ltransitivity;[solve[find_Lrewrite_lemma]|]
    end)
  end.

Ltac LrewriteSimpl' := let flag := fresh in assert (flag:=tt);
  (tryif Lbeta then try LrewriteSimpl'' flag else LrewriteSimpl'' flag);try clear flag.

Ltac LrewriteSimpl := Lrewrite_wrapper ltac:(idtac;LrewriteSimpl').

  (*
  From Ltac2 Require Import Ltac2.
  Ltac2 rec lrewriteSimpl' () :=
    (* time "LrewriteSimpl'" *)
    lazy_match! goal with
    | [ |- _ (@ext _ (@TyB _ ?reg) _ _) _ ] => eapply ext_rel_helper (* for backwards-compability, if used on term with hole*)
    | [ |- _ (@extT _ (@TyB _ ?reg) _ _ _) _] => eapply extT_rel_helper (* for backwards-compability, if used on term with hole*)
    | [ |- ?rel ?s _ ] => ltac1:(has_no_evar &s) (* ;idtac "head" s *)
    end ;
    lazy_match! goal with
    | [ |- ?rel (L.app _ _) _] =>
      (* first reduce recursively *)
      (lazy_match! rel with
       |  star step => ltac1:(refine (pow_app_helper _ _ _))
       | redLe _ => ltac1:(refine (redLe_app_helper _ _ _))
       end)  > [lrewriteSimpl' ();ltac1:(Lreflexivity)..| ]  ;

      (* then reduce here/above *)
      lazy_match! goal with
           (* beta-reduce here & recurse down again (if argument abstraction)*)
         | [ |- _ (L.app (lam _) ?t) _ ] =>
             let valt := Fresh.in_goal @H in
             assert (valt:proc t) by ltac1:(Lproc);
             ltac1:(Lbeta);
             lazy_match! goal with
               [ |- _ (L.app (lam _) t) _] => Control.backtrack_tactic_failure "could not reduce"
             | [ |- _] => ()
             end;
             Std.clear [valt];(lrewriteSimpl' ())
           | [ |- _] =>

             let appTimeHelper _:=
                  (lazy_match! goal with
                  | [ |- app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _ ]
                    => let rr := Fresh.in_goal @R in
                      specialize (extTApp &fInts &xInts) as rr;
                      lazy_match! Constr.type &rr with
                        (* As we might build n using the projection on an on-ty-fly constructed computableTime-instance, we mustavoid it to depend on the proof that the time function is correct*)
                        | ?s >(<= ?n) ?t =>
                          let n' := Std.eval_unfold [(reference:(&evalTime), Std.AllOccurrences)] &n in
                              change (&s >(<= &n') t) in rr
                      end;
                      ltac1:(Ltransitivity)> [exact &rr|]
                 end) in

             (* use correctness lemmates of int here*)
             lazy_match! goal with
             | [ |- L.app (@ext _ (_ ~> _ ) _ _) (ext _) >* _] => ltac1:(Ltransitivity) > [apply extApp|]
             | [ |- L.app (@ext _ (_ ~> _ ) _ ?ints) (@enc _ ?reg ?x) >* ?v ]=>
               change (app (@ext _ _ _ &ints) (@ext _ _ _ (reg_is_ext &reg &x)) >* &v);
               ltac1:(Ltransitivity) > [apply extApp|]

             | [ |- L.app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _ ]=> appTimeHelper ()
             | [ |- L.app (@extT _ (_ ~> _ ) _ _ ?ints) (@enc _ ?reg ?x) >(<= ?k ) ?v ]=>
               change (L.app (@extT _ _ _ _ &ints) (@extT _ _ _ _ (reg_is_extT &reg &x)) >(<= &k) &v);appTimeHelper ()
             | [ |- _ ]=> ()

             end
           end
    | [|- _] => ()
    end;
    let rec loop () :=  ltac1:(Ltransitivity)> [ltac1:(find_Lrewrite_lemma)|lrewriteSimpl' ()];try (loop ()) in
    try (loop ()) ;
    try ((ltac1:(Ltransitivity) > [ltac1:(useFixHypo)|]));
    (* clean up goal*)
    lazy_match! goal with
    | [ |- _ (@ext _ (@TyB _ ?reg) _ _) _] => eapply ext_rel_helper
    | [ |- _ (@extT _ (@TyB _ ?reg) _ _ _) _] => eapply extT_rel_helper
    | [ |- _ ]=> ()
    end.

  Ltac LrewriteSimpl' ::= ltac2:(lrewriteSimpl' ()). *)

repo: time-invariance-thesis-for-L


text:
Set Warnings "-notation-overridden,-parsing".
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Import Tweetnacl.Low.M.
Require Import Tweetnacl.Low.S.
Require Import Tweetnacl_verif.init_tweetnacl.
Require Import Tweetnacl_verif.spec_M.
Require Import Tweetnacl_verif.spec_S.

Open Scope Z.

Import Low.

Definition Gprog : funspecs :=
      ltac:(with_library prog [M_spec; S_spec]).

Lemma body_S: semax_body Vprog Gprog f_S S_spec.
Proof.
start_function.
unfold nm_overlap_array_sep_2.
flatten ; Intros.
1: subst o v_a.
1: forward_call (v_o,v_o,v_o,sho,sho,sho,(mVI64 a),a,a,3).
1: unfold_nm_overlap_array_sep; simpl; entailer!.
1: repeat match goal with | [ |- _ /\ _ ] => split; auto end.
2: forward_call (v_o,v_a,v_a,sho,sha,sha,o,a,a,2).
2: unfold_nm_overlap_array_sep; simpl; entailer!.
2: repeat match goal with | [ |- _ /\ _ ] => split; auto end.
all: unfold_nm_overlap_array_sep ; simpl.
all: forward.
all: unfold_nm_overlap_array_sep.
all: unfold S.
all: rewrite Eq.
all: entailer!.
all: apply M_Zlength ; assumption.
Qed.

Close Scope Z.

author: ildyria

repo: coq-verif-tweetnacl


text:
(* This file contains the formalisation of lemma 24 and corollary 25 *)

Require Import general.
Require Import iterms.
Require Import lterms.
Require Import standard.
Require Import erasure.
Require Import sred.
Require Import ared.
Require Import ired.
Require Import istd.
Require Import acommute.
Require Import aexpand.
Require Import astd.

(* lemma 24 *)
Lemma lem_exp_a_preserves_leadsto_f1 :
  forall t t', Leadsto t' F1 -> Contr_clc_a t t' -> Leadsto t F1.
Proof.
  unfold Leadsto; yintros; split.
  pose lem_a_strongly_standard; ycrush.
  unfold StronglyStandard; intros.
  assert (exists u, Red_clc_s t' u /\ (Contr_clc_a x u \/ u = x)).
  pose lem_a_commute_red; ycrush.
  simp_hyps.
  destruct H5.
  Reconstr.hobvious (@H3, @H5)
		    (@ared.lem_contr_a_snf)
		    Reconstr.Empty.
  ycrush.
Qed.

Lemma lem_exp_red_i_a_preserves_leadsto_f1 :
  forall t t', Leadsto t' F1 -> Red_clc_i_a t t' -> Leadsto t F1.
Proof.
  assert (forall t t', Red_clc_i_a t t' -> Leadsto t' F1 -> Leadsto t F1).
  intros t t' H.
  induction H; yisolve.
  destruct H.
  pose lem_contr_exp_i_preserves_leadsto_f1; pose lem_contr_exp_i; ycrush.
  pose lem_exp_a_preserves_leadsto_f1; ycrush.
  ycrush.
Qed.

(* corollary 25 *)
Corollary cor_expansion :
  forall t q q', Leadsto t F1 -> Erasure t q -> Contr_clc0 q' q ->
                 exists t', Erasure t' q' /\ Leadsto t' F1.
Proof.
  intros.
  assert (exists t', Red_clc_i_a t' t /\ Erasure t' q').
  pose lem_clc0_expansion; pose lem_strongly_standard_implies_standard; unfold Leadsto in *; ycrush.
  pose lem_exp_red_i_a_preserves_leadsto_f1; ycrush.
Qed.

author: lukaszcz

repo: clc

save_path: github-repos/coq/lukaszcz-clc


Require Import Arith.
Require Import Omega.
Require Import String.
Require Import List.

(*
 * Simple filesystem model for 260 project.
 *
 * This has:
 *    lookup
 *    create
 *    unlink
 *    read
 *    write
 *    truncate
 *    fsync
 *    getroot
 *    sync
 *
 * It is (for now) written using its own abstract syntax on the
 * grounds that (a) this lets me get started writing it, (b) changing
 * that around later is relatively straightforward, and (c) injecting
 * AST into a monad is a lot easier than the other way around.
 *)

(*************************************************************)
(* AST *)

Inductive Expr: Type -> Type :=
| value: forall t, t -> Expr t
| cond: forall t, Expr bool -> Expr t -> Expr t -> Expr t
.

Inductive Stmt: Type :=
| block: list Stmt -> Stmt
| assign: forall t, Var t -> Expr t -> Stmt
| if: Expr bool -> Stmt -> Stmt -> Stmt
| while: Expr bool -> Stmt -> Stmt
| call: forall t, Var t -> Proc t -> Stmt
.

(*
 * Extended/sugary AST forms
 *)

Definition coqcall (f : ta -> tr) (x : ta): Expr tr :=
   value (f x)
.

Definition skip: Stmt := block [].

(*************************************************************)
(* directory support *)

Definition roosterfs_searchdir dir name fs: option buffer :=
   {{ vnode_is_locked dir }}
   block [
	local slot;
	local lastslot;
	local ret;
	local lbn;
	local buf;
	local sm;
	local found;

	slot ::== value 0;
	lastslot ::== fieldof dir size;
	ret ::== value None;
	while (slot < lastslot) (block [
		lbn ::== slot / dirslots_per_block;
		buf ::== roosterfs_metaread dir lbn fs;
		sm ::== buf.metadata;
		found := value (
			match StringMap.find name sm with
			| Some _ => true
			| None => false
			end);
		if found (block [
			ret := Some buf;
			break;
		]) (*else*) skip;
		buf_release buf;
	]);
	return ret;
   ]
   {{ ret = None \/ (exists vn, ret = Some vn /\ hasreference vn) }}
   {{ True }} (* crash condition *)
.

(*************************************************************)
(* vnops *)

Definition roosterfs_lookup dir name fs: option roosterfs_vnode :=
   block [
	vnode_lock dir fs;
	optdirbuf := roosterfs_searchdir dir name fs;
	found := coqcall issome optdirbuf;
	if found (block [
		dirbuf := coqcall wassome optdirbuf;
		sm := dirbuf.metadata;
		ino := value (match StringMap.find name sm with
			| Some ino -> ino
			| None -> 0 (* impossible *)
			end);
		ret := roosterfs_loadvnode ino fs;
		buf_release buf;
	]) (*else*) (block [
		ret := None;
	]);
	vnode_unlock dir fs;
	return ret;
   ]
.

Definition roosterfs_create dir name fs: option roosterfs_vnode :=
   block [
	vnode_lock dir fs;
	optdirbuf := roosterfs_searchdir dir name fs;
	found := coqcall issome optbuf;
	if found (block [
		ret := None;
	]) (*else*) (block [
		dirbuf := coqcall wassome optdirbuf;
		sm := dirbuf.metadata;
		optinobuf := roosterfs_ialloc fs;
		worked := coqcall issome optinobuf;
		if worked (block [
			(inobuf, ino) := wassome optinobuf;
			dino := inobuf.metadata;
			dino.type = ROOSTERFS_FILE;
			dino.size = 0;
			dino.linkcount = 1;
			dino.blockmap = IntMap.empty;
			dino.corrupt = false;
			inobuf.metadata := dino;
			roosterfs_journal_zerodino ino;
			roosterfs_journal_type ino ROOSTERFS_INVALID
							ROOSTERFS_FILE;
			roosterfs_journal_linkcount ino 0 1;
			buffer_mark_dirty inobuf;

			ret := roosterfs_loadvnode_frombuf ino inobuf fs;
			worked := coqcall issome ret;
			if worked (block [
				sm := StringMap.add name ino sm;
				dirbuf.metadata := sm;
				roosterfs_journal_diradd dirino name ino;
				buffer_mark_dirty dirbuf;
			]) (*else*) (block [
				roosterfs_ifree ino fs;
			]);
			buffer_release buf;
			buffer_release inobuf;
		]) (*else*) (block [
			buf_release optbuf;
			ret := None;
		])
	]);
	vnode_unlock dir fs;
	return ret;
   ]
.

(* XXX; but let's make the above compile first
Definition roosterfs_unlink dir name fs: option roosterfs :=
   block [
	vnode_lock dir fs;
	vnode_unlock dir fs;
	return ret;
   ]
.

Definition roosterfs_read vn len offset fs: option bytes :=
   block [
	vnode_lock vn fs;
	vnode_unlock vn fs;
	return ret;
   ]
.

Definition roosterfs_write vn bytes offset fs: option roosterfs :=
   block [
	vnode_lock vn fs;
	vnode_unlock vn fs;
	return ret;
   ]
.

Definition roosterfs_truncate vn len fs: option roosterfs :=
   block [
	vnode_lock vn fs;
	vnode_unlock vn fs;
	return ret;
   ]
.

Definition roosterfs_fsync vn fs: option roosterfs :=
   block [
	vnode_lock dir fs;
	vnode_unlock dir fs;
	return ret;
   ]
.

Definition roosterfs_getroot fs: roosterfs_vnode :=
   block [
	vnode_lock dir fs;
	vnode_unlock dir fs;
	return ret;
   ]
.

Definition roosterfs_sync fs: roosterfs :=
   block [
	vnode_lock dir fs;
	vnode_unlock dir fs;
	return ret;
   ]
.
*)


text:
(*-------------------------------------------------------------------- *)
From mathcomp Require Import all_ssreflect.
From mathcomp.analysis Require Import boolp.

(* -------------------------------------------------------------------- *)
Import Order Order.Theory.

Local Open Scope nat_scope.
Local Open Scope order_scope.

(* -------------------------------------------------------------------- *)
Set   Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Unset SsrOldRewriteGoalsOrder.

Obligation Tactic := move=> /=.

(* -------------------------------------------------------------------- *)
Definition chain {d : unit} [T : porderType d] (c : nat -> T) :=
  forall i : nat, c i <= c i.+1.

(* -------------------------------------------------------------------- *)
Section ChainTheory.
Context {d : unit} {T : porderType d}.

Lemma chain_shift (c : nat -> T) : chain c -> chain (c \o succn).
Proof. by move=> ch_c i /=; apply: ch_c. Qed.

Lemma chain_homo (c : nat -> T) :
  chain c -> {homo c : x y / (x <= y)%N >-> (x <= y)}.
Proof.
move=> cc x y /subnK => <-; elim: (y - x) => //= n ih.
by rewrite addSn; apply: (le_trans ih); apply: cc.
Qed.
End ChainTheory.

(* -------------------------------------------------------------------- *)
Module Cpo.
Section ClassDef.

Record mixin_of
  (T0 : Type) (b : POrder.class_of T0) (T := POrder.Pack tt b) := Mixin
{
  bot : T;
  lub : (nat -> T) -> T;
  _   : forall x, bot <= x;
  _   : forall c : nat -> T, chain c -> forall i, c i <= lub c;
  _   : forall c : nat -> T, chain c -> forall x, (forall i, c i <= x) -> lub c <= x;
}.

Set Primitive Projections.
Record class_of (T : Type) := Class {
  base  : POrder.class_of T;
  mixin : mixin_of base;
}.
Unset Primitive Projections.

Local Coercion base : class_of >-> POrder.class_of.

Structure type (disp : unit) := Pack { sort; _ : class_of sort }.

Local Coercion sort : type >-> Sortclass.

Variables (T : Type) (disp : unit) (cT : type disp).

Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack disp T c.
Definition clone_with disp' c of phant_id class c := @Pack disp' T c.

Definition pack :=
  fun bT b & phant_id (@POrder.class disp bT) b =>
  fun m => Pack disp (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition porderType := @POrder.Pack disp cT class.
End ClassDef.

Module Exports.
Coercion base : class_of >-> POrder.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Coercion choiceType : type >-> Choice.type.
Coercion porderType : type >-> POrder.type.
Canonical eqType.
Canonical choiceType.
Canonical porderType.
Notation cpoType  := type.
Notation CpoType T m := (@pack T _ _ _ id m).
Notation "[ 'cpoType' 'of' T 'for' cT ]" := (@clone T _ cT _ id)
  (at level 0, format "[ 'cpoType'  'of'  T  'for'  cT ]") : form_scope.
Notation "[ 'cpoType' 'of' T 'for' cT 'with' disp ]" :=
  (@clone_with T _ cT disp _ id)
  (at level 0, format "[ 'cpoType'  'of'  T  'for'  cT  'with'  disp ]") :
  form_scope.
Notation "[ 'cpoType' 'of' T ]" := [cpoType of T for _]
  (at level 0, format "[ 'cpoType'  'of'  T ]") : form_scope.
Notation "[ 'cpoType' 'of' T 'with' disp ]" :=
  [cpoType of T for _ with disp]
  (at level 0, format "[ 'cpoType'  'of'  T  'with' disp ]") : form_scope.
End Exports.
End Cpo.

Export Cpo.Exports.

Definition bot {disp : unit} {T : cpoType disp} : T :=
  Cpo.bot (Cpo.class T).

Definition lub {disp : unit} {T : cpoType disp} (c : nat -> T) : T :=
  Cpo.lub (Cpo.class T) c.

(* -------------------------------------------------------------------- *)
Module CpoMixin.
Section CpoMixin.
Context {disp : unit} (T : porderType disp).

Record of_ := Build {
  bot       : T;
  lub       : (nat -> T) -> T;
  le0c      : forall x, bot <= x;
  lub_ub    : forall c : nat -> T, chain c -> forall i, c i <= lub c;
  lub_least : forall c : nat -> T, chain c -> forall x, (forall i, c i <= x) -> lub c <= x;
}.

Definition cpoMixin (m : of_) :=
  @Cpo.Mixin _ _ (bot m) (lub m) (le0c m) (lub_ub m) (lub_least m).
End CpoMixin.

Module Exports.
Coercion cpoMixin : of_ >-> Cpo.mixin_of.
Notation cpoMixin := of_.
Notation CpoMixin := Build.
End Exports.
End CpoMixin.

Import CpoMixin.Exports.

(* -------------------------------------------------------------------- *)
Section CPOTheory.
Context {d : unit} {T : cpoType d}.

Lemma le0c (x : T) : bot <= x.
Proof. by case: T x => ? [? []]. Qed.

Hint Extern 0 (is_true (bot <= _)) => (exact: le0c) : core.

Lemma lub_ub (c : nat -> T): chain c -> forall i, c i <= lub c.
Proof. by case: T c => ? [? []]. Qed.

Lemma lub_least (c : nat -> T):
  chain c -> forall x, (forall i, c i <= x) -> lub c <= x.
Proof. by case: T c => ? [? []]. Qed.

Lemma lub_shift (c : nat -> T): chain c -> lub (c \o succn) = lub c.
Proof.
move=> sc_c; rewrite (rwP eqP) eq_le; apply/andP; split.
- apply: lub_least; first by apply: chain_shift.
  by move=> i /=; apply: lub_ub.
- apply: lub_least => // -[|n].
  - by apply/(le_trans (sc_c 0%N))/lub_ub/chain_shift.
  - by apply/lub_ub/chain_shift.
Qed.
End CPOTheory.

(* -------------------------------------------------------------------- *)
Module ScottContinuous.
Section ClassDef.
Context {dU dV : unit} (U : cpoType dU) (V : cpoType dV).

Definition axiom (f : U -> V) :=
  [/\ forall c, chain c -> chain (f \o c)
    & forall c, chain c -> f (lub c) = lub (f \o c)].

Structure map (phUV : phant (U -> V)) := Pack {apply; _ : axiom apply}.
Local Coercion apply : map >-> Funclass.

Variables (phUV : phant (U -> V)) (f g : U -> V) (cF : map phUV).
Definition class := let: Pack _ c as cF' := cF return axiom cF' in c.
Definition clone fA of phant_id g (apply cF) & phant_id fA class :=
  @Pack phUV f fA.

End ClassDef.

Module Exports.
Notation scott f := (axiom f).
Coercion apply : map >-> Funclass.
Notation Scott fA := (Pack (Phant _) fA).
Notation "{ 'scott' fUV }" := (map (Phant fUV))
  (at level 0, format "{ 'scott'  fUV }") : order_scope.
Notation "[ 'scott' 'of' f 'as' g ]" := (@clone _ _ _ f g _ _ idfun id)
  (at level 0, format "[ 'scott'  'of'  f  'as'  g ]") : form_scope.
Notation "[ 'scott' 'of' f ]" := (@clone _ _ _ f f _ _ id id)
  (at level 0, format "[ 'scott'  'of'  f ]") : form_scope.
End Exports.
End ScottContinuous.

Include ScottContinuous.Exports.

(* -------------------------------------------------------------------- *)
Section SCTheory.
Context {dT dU : unit} {T : cpoType dT} {U : cpoType dU} (f : {scott T -> U}).

Lemma sc_chain c : chain c -> chain (f \o c).
Proof. by move: c; case: f => ? []. Qed.

Lemma sc_lub c : chain c -> f (lub c) = lub (f \o c).
Proof. by move: c; case: f => ? []. Qed.

Lemma homo_sc : {homo f : x y / x <= y}.
Proof.
move=> x y le_xy; pose c n := if n is 0 then x else y.
by have/(_ 0): chain (f \o c) by apply: sc_chain; case.
Qed.
End SCTheory.

(* -------------------------------------------------------------------- *)
Section LFP.
Context {d : unit} {T : cpoType d} (f : {scott T -> T}).

Definition chaini i := iter i f bot.

Lemma chain_iter : chain chaini.
Proof. by elim=> [|n ih]; [apply: le0c | apply: homo_sc]. Qed.

Lemma chaini_shift : chaini \o succn = f \o chaini.
Proof. by []. Qed.

Hint Extern 0 (chain chaini) => (exact: chain_iter) : core.

Lemma fp_lub_chaini : f (lub chaini) = lub chaini.
Proof. by rewrite sc_lub // -chaini_shift lub_shift. Qed.

Lemma least_fp_lub_chaini x : f x = x -> lub chaini <= x.
Proof.
move=> fp_x; apply: lub_least => //.
elim=> /= [|n ih]; first by apply: le0c.
by rewrite -fp_x; apply: homo_sc.
Qed.
End LFP.

(* -------------------------------------------------------------------- *)
Section PointedCPO.
Definition pointed (T : Type) := option T.

Canonical pointed_eqType     (T : eqType    ) := [eqType     of pointed T].
Canonical pointed_choiceType (T : choiceType) := [choiceType of pointed T].
Canonical pointed_countType  (T : countType ) := [countType  of pointed T].

Section Def.
Context {T : choiceType}.

Definition ple (x y : pointed T) : bool :=
  x \in [:: None; y].

Definition plt (x y : pointed T) : bool :=
  ~~ x && y.

Program Definition pointed_lePOrderMixin : lePOrderMixin _ :=
  @LePOrderMixin _ ple plt _ _ _ _.

Next Obligation.
move=> x y; rewrite /ple /plt mem_seq2.
by case: x y => [x|] [y|] //=; rewrite eq_sym andNb.
Qed.

Next Obligation.
by case=> // x; rewrite /ple mem_seq2 eqxx orbT.
Qed.

Next Obligation.
by case=> [x|] [y|] //=; rewrite /ple !mem_seq2 !orFb => /andP [] /eqP.
Qed.

Next Obligation.
case=> [y|] [x|] [z|] //=; rewrite /ple !mem_seq2.
by rewrite !orFb => /eqP[->] /eqP[->].
Qed.

Canonical pointed_POrderType :=
  POrderType NatOrder.nat_display (pointed T) pointed_lePOrderMixin.

Lemma pleE (x y : pointed T) : (x <= y) = ple x y.
Proof. by []. Qed.

Lemma pltE (x y : pointed T) : (x < y) = plt x y.
Proof. by []. Qed.

Lemma ple_Some (x y : T) : (Some x <= Some y :> pointed T) = (x == y).
Proof.
apply/idP/eqP => [|->//]; rewrite pleE.
by rewrite /ple mem_seq2 orFb => /eqP[].
Qed.

Definition pbot : pointed T := None.

Definition plub (c : nat -> pointed T) : pointed T :=
  if pselect (chain c) then
    if pselect (exists i, c i != None) is left h then
      c (xchoose h) else None
  else None.

Lemma pbot_bot (x : pointed T) : pbot <= x.
Proof. by []. Qed.

Lemma pchainP (c : nat -> pointed T) : chain c <->
  (exists2 i,
       (forall j, (j <  i)%N -> c j = None)
     & (forall j, (j >= i)%N -> c j = c i)).
Proof. split; last first.
- case=> i lti gei j; case: (ltnP j i); first by move=> /lti ->.
  by move=> le_ij; rewrite !gei // (leq_trans le_ij).
move=> cc; case: (pselect (exists i : nat, c i != None)); last first.
- move=> h; have cE: forall j, c j = None.
  - move=> j; apply/eqP; rewrite -[_ == _]negbK.
    by apply/negP => ?; apply: h; exists j.
  by exists 0 => // j _; rewrite !cE.
move=> h; exists (ex_minn h) => j.
- case: ex_minnP=> m cmE hmin; apply: contraTeq.
  by move/hmin; rewrite leqNgt.
- case: ex_minnP=> m; case cmE: (c m) => [x|] //.
  move=> _ hmin le_mj; have: (Some x <= c j :> pointed T).
  - by rewrite -cmE; apply: chain_homo.
  by case: (c j) => //= y; rewrite ple_Some => /eqP->.
Qed.

Program Definition pointed_cpo : Cpo.mixin_of _ :=
  @CpoMixin _ _ pbot plub _ _ _.

Next Obligation. by []. Qed.

Next Obligation.
move=> c /[dup] cc /pchainP[i lti gei] j; case: (ltnP j i).
- by move/lti=> ->; apply: pbot_bot.
move/gei=> ->; case ciE: (c i) => [x|] //; rewrite /plub.
case: pselect => //= _; case: pselect => /=; last first.
- by case; exists i; rewrite ciE.
move=> h; set k := xchoose _; suff: (i <= k)%N.
- by move/gei=> ->; rewrite ciE.
rewrite leqNgt; apply/negP=> /lti ckE.
by move: (xchooseP h); rewrite ckE eqxx.
Qed.

Next Obligation.
move=> c /[dup] cc /pchainP[i lti gei] x ub_x.
by rewrite /plub; case: pselect => //= _; case: pselect.
Qed.

Canonical pointed_cpoType := CpoType (pointed T) pointed_cpo.

Lemma plubE (c : nat -> pointed T) : chain c -> lub c =
  if pselect (exists i, c i != None) is left h then
    c (ex_minn h)
  else bot.
Proof.
move=> cc; rewrite /lub /= /plub; case: pselect => //= _.
case: pselect => // h; case: ex_minnP=> m cmE hmin.
have /hmin /(chain_homo cc) {hmin} := xchooseP h.
case: (c m) cmE => // x _; case: (c _) => // y.
by rewrite ple_Some => /eqP ->.
Qed.
End Def.
End PointedCPO.

author: coq-quantum

repo: CoqQ

save_path: github-repos/coq/coq-quantum-CoqQ