text:
Require Import VST.floyd.proofauto.
Require Import VST.progs.field_loadstore.

Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Local Open Scope logic.

Definition t_struct_b := Tstruct _b noattr.

Definition sub_spec (sub_id: ident) :=
 DECLARE sub_id
  WITH v : val * list (val*val) , gv: globals
  PRE  []
        PROP  (is_int I8 Signed (snd (nth 1%nat (snd v) (Vundef, Vundef))))
        PARAMS() GLOBALS (gv)
        SEP   (data_at Ews t_struct_b v (gv _p))
  POST [ tvoid ]
        PROP() RETURN()
        SEP(data_at Ews t_struct_b (snd (nth 1%nat (snd v) (Vundef, Vundef)), snd v) (gv _p)).

Definition sub_spec' (sub_id: ident) :=
 DECLARE sub_id
  WITH v : reptype t_struct_b, gv: globals
  PRE  []
        PROP  (is_int I8 Signed (proj_reptype _ (DOT _y2 SUB 1 DOT _x2) v))
        PARAMS() GLOBALS (gv)
        SEP   (data_at Ews t_struct_b v (gv _p))
  POST [ tvoid ]
        PROP() RETURN()
        SEP(data_at Ews t_struct_b
           (upd_reptype t_struct_b (DOT _y1) v
             (proj_reptype t_struct_b (StructField _x2 :: ArraySubsc 1 :: StructField _y2 :: nil) v))
           (gv _p)).

Lemma spec_coincide: sub_spec' = sub_spec.
Proof.
(*reflexivity.*)
Abort.

Definition Gprog : funspecs :=   ltac:(with_library prog [
    sub_spec _sub1; sub_spec _sub2; sub_spec _sub3]).

Lemma body_sub1:  semax_body Vprog Gprog f_sub1 (sub_spec _sub1).
Proof.
  unfold sub_spec.
  start_function.
  forward.
  forward.
  entailer!.
Qed.

Lemma body_sub2:  semax_body Vprog Gprog f_sub2 (sub_spec _sub2).
Proof.
  unfold sub_spec.
  start_function.
  forward.
  forward.
  forward.
  entailer!.
Qed.

Lemma body_sub3:  semax_body Vprog Gprog f_sub3 (sub_spec _sub3).
Proof.
  unfold sub_spec.
  start_function.
  forward.
  forward.
  forward.
  forward.
  entailer!.
Qed.

author: anshumanmohan

repo: CertiGraph-VST


text:
(* Exercises on Category Theory in UniMath *)
(* for lecture by Peter LeFanu Lumsdaine, Thu 2017-12-14 *)
(* School and Workshop on Univalent Maths, Birmingham 2017 *)
(* https://unimath.github.io/bham2017/ *)

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Core.Setcategories.
Require Import UniMath.CategoryTheory.categories.HSET.All.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.limits.FinOrdProducts.
Require Import UniMath.CategoryTheory.limits.equalizers.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Monads.Monads.
Require Import UniMath.Combinatorics.StandardFiniteSets.
Require Import UniMath.CategoryTheory.limits.binproducts.

Local Open Scope cat.

(* NOTE: some of these exercises (or parts of them) are straightforward, while other parts are intended to be quite difficult.  So I don’t recomment aiming to complete them in order — if stuck on a difficult part, move on and come back for another attempt later!

Skeleton solutions and hints are provided, to exhibit good tools and techniques for working with categories.  However, you may well want to add extra definitions/lemmas besides the ones suggested in the skeleton. *)

Section Exercise_0.
(** Univalent categories

  Show that in any univalent category, the type of objects has h-level 3 *)

  Proposition isofhlevel3_ob_of_univalent_cat (C : category) (H : is_univalent C)
    : isofhlevel 3 (ob C).
  Proof.
  Admitted.

End Exercise_0.

Section Exercise_1.
(** Non-univalent categories

  Problem: Construct the category with objects the natural numbers, and with maps m->n all functions {1,…,m}->{1,…,n}.  Show that this is a set-category, and that it is NOT univalent.

  Hint: for defining categories (and other large multi-component structures), it’s usually better to define them a few components at a time, following the structure of the definition, as the following skeleton suggests.

  An alternative approach is to go directly for the total structure [Definition nat_category : category], then begin with [use makecategory.] and construct the whole thing in a single interactive proof.  This approach can be good for first finding a proof/construction; but it often causes speed issues down the line, because the resulting term is very large. *)

  Definition nat_category_ob_mor : precategory_ob_mor.
  Proof.
  Admitted.

  Definition nat_category_data : precategory_data.
  Proof.
  Admitted.

  Definition nat_category_is_precategory : is_precategory nat_category_data.
  Proof.
  Admitted.

  Definition nat_category : category.
  Proof.
  Admitted.

  Definition nat_setcategory : setcategory.
  Proof.
  Admitted.

  Proposition nat_category_not_univalent : ¬ (is_univalent nat_category).
  Proof.
  Admitted.

End Exercise_1.

Section Exercise_2.
  (* Exercise 2.1: Define `pointed_disp_cat` with `disp_struct`. *)
  Definition pointed_disp_cat
    : disp_cat SET.
  Proof.
  Admitted.

  (* Exercise 2.2: Define a displayed category on sets of a binary operation on them.
     The displayed objects over `X` are maps `X × X → X` and the displayed morphisms over `f` are proofs that `f` preserves the operation.
   *)
  Definition operation_disp_cat
    : disp_cat SET.
  Proof.
  Admitted.

  (* Using the product of displayed categories, we now define *)
  Definition pointed_operation_disp_cat
    : disp_cat SET.
  Proof.
    use dirprod_disp_cat.
    - exact pointed_disp_cat.
    - exact operation_disp_cat.
  Defined.

  (* This gives rise to a total category *)
  Definition pointed_operation_set
    : category
    := total_category pointed_operation_disp_cat.

  (* For convenience, we define some projection to access the structure *)
  Definition carrier
             (X : pointed_operation_set)
    : hSet
    := pr1 X.

  Definition unit_el
             (X : pointed_operation_set)
    : carrier X.
  Proof.
  Admitted.
  (* Once defined, the following should type check. *)
  (* := pr12 X. *)

  Definition mul
             (X : pointed_operation_set)
    : carrier X → carrier X → carrier X.
  Admitted.
  (* Once defined, the following should type check. *)
  (* := λ x y, pr22 X (x ,, y). *)

  (* Exercise 2.3: Define the category of monoid displayed category.
     Hint: use `disp_full_sub`.
   *)
  Definition monoid_laws_disp_cat
    : disp_cat pointed_operation_set.
  Proof.
  Admitted.

  Definition monoids
    : category
    := total_category monoid_laws_disp_cat.

  (* During the lecture, we already showed that pointed sets are univalent as follows *)
  Definition pointed_is_univalent_disp
    : is_univalent_disp pointed_disp_cat.
  Proof.
  Admitted.
  (* Once everything is in place, the following proof should work. *)
  (*
    apply is_univalent_disp_from_fibers.
    intros X x₁ x₂.
    use isweqimplimpl.
    - intros f.
      apply f.
    - apply X.
    - apply isaproptotal2.
      + intro.
        apply isaprop_is_iso_disp.
      + intros p q r₁ r₂.
        apply X.
  Defined.
   *)

  (* Exercise 2.4: Show that each part gives rise to a displayed univalent category and conclude that the total category is univalent.
     Hint: adapt the proof from the lecture notes.
   *)
  Definition operation_is_univalent_disp
    : is_univalent_disp operation_disp_cat.
  Proof.
    apply is_univalent_disp_from_fibers.
  Admitted.

  (* Now we conclude *)
  Definition pointed_operation_is_univalent_disp
    : is_univalent_disp pointed_operation_disp_cat.
  Proof.
    use dirprod_disp_cat_is_univalent.
    - exact pointed_is_univalent_disp.
    - exact operation_is_univalent_disp.
  Defined.

  Definition pointed_operation_is_univalent
    : is_univalent pointed_operation_set.
  Proof.
    apply is_univalent_total_category.
    - exact is_univalent_HSET.
    - exact pointed_operation_is_univalent_disp.
  Defined.

  (* Exercise 2.5: conclude that the category of monoids is univalent. *)
  Definition monoid_is_univalent_disp
    : is_univalent_disp monoid_laws_disp_cat.
  Proof.
  Admitted.

  Definition monoids_is_univalent
    : is_univalent monoids.
  Proof.
    apply is_univalent_total_category.
    - exact pointed_operation_is_univalent.
    - exact monoid_is_univalent_disp.
  Defined.
End Exercise_2.

Section Exercise_3.
(** Limits and colimits.

  1. Define the empty graph and empty diagram, and show that any limit of the empty diagram is a terminal object in the directly-defined sense.
*)

  Definition empty_graph : graph.
  Proof.
  Admitted.

  Definition empty_diagram (C : category) : diagram empty_graph C.
  Proof.
  Admitted.

  Definition isTerminal_limit_of_empty_diagram
      {C} (L : LimCone (empty_diagram C))
    : isTerminal _ (lim L).
  Proof.
  Admitted.

  (* 2. Show that for a univalent category, “having an initial object” is a property. *)
  Definition isaprop_initial_obs_of_univalent_category
      {C : univalent_category}
    : isaprop (Initial C).
  Proof.
  Admitted.

  (* 3. Show that if a category has equalisers and finite products, then it has pullbacks *)
  Definition pullbacks_from_equalizers_and_products {C : category}
    : Equalizers C -> BinProducts C -> Pullbacks C.
  Proof.
  Admitted.

End Exercise_3.

Section Exercise_4.
(** Functors and natural transformations / monads and adjunctions

Prove that an adjunction induces a monad.  Construct the Kleisli category of a monad.  Show that the Kleisli construction does not preserve univalence: that is, give an example of a monad on a univalent category whose Kleisli category is not univalent. *)

  (* Hint: as usual, it may be helpful to break out parts of these multi-component structures as separate definitions. *)

  Definition monad_from_adjunction {C D : category}
      (F : functor C D) (G : functor D C) (A : are_adjoints F G)
    : Monad C.
  Proof.
  Admitted.

  Definition kleisli_cat {C : category} (T : Monad C) : category.
  Proof.
    (* see <https://en.wikipedia.org/wiki/Kleisli_category> *)
  Admitted.

  Theorem kleisli_breaks_univalence
    : ∑ (C : univalent_category) (T : Monad C), ¬ is_univalent (kleisli_cat T).
  Proof.
  Admitted.

End Exercise_4.

author: UniMath

repo: Schools

save_path: github-repos/coq/UniMath-Schools


text:
Require Import Omega.
Require Import RelationClasses.

From sflib Require Import sflib.

From PromisingLib Require Import Axioms.
From PromisingLib Require Import Basic.
From PromisingLib Require Import DataStructure.
From PromisingLib Require Import Loc.

Require Import Time.
Require Import Event.
From PromisingLib Require Import Language.
Require Import View.
Require Import Cell.
Require Import Memory.
Require Import TView.
Require Import Thread.
Require Import Configuration.
Require Import Progress.

Require Import MemoryRel.
Require Import SmallStep.
Require Import Fulfilled.
Require Import ReorderPromise.
Require Import Race.
Require Import PromiseConsistent.
Require Import PIStep.

Set Implicit Arguments.

Inductive is_reading_writing_promise_except tid c : Prop :=
| is_reading_promise_except_intro
    e lang st1 st2 loc val ord tid' to'
    (ST1: option_map fst (IdentMap.find tid c.(Configuration.threads)) = Some (existT _ lang st1))
    (NOWR: lang.(Language.step) e st1 st2)
    (RW: ProgramEvent.is_reading e = Some(loc, val, ord) \/ ProgramEvent.is_writing e = Some(loc, val, ord))
    (NEQ: tid' <> tid)
    (PROM: Threads.is_promised tid' loc to' c.(Configuration.threads))
.

Lemma pi_consistent_lang_step_pi_rw
      tid cST1 cST2
      (WF: pi_wf loctmeq cST1)
      (PI_CONSISTENT: pi_consistent cST1)
      (PI_RACEFREE: pf_racefree cST1.(fst))
      (PI_STEPS: rtc (pi_step_evt true tid) cST1 cST2)
      (PRCONS: forall tid0, promise_consistent_th tid0 cST2.(snd)):
  ~ is_reading_writing_promise_except tid cST2.(snd).
Proof.
  ii. inv H. inv PROM.
  inv PI_CONSISTENT. ss.
  guardH RW. destruct cST2 as [cS2 cT2].

  eapply rtc_implies in PI_STEPS; [|eapply pi_step_evt_to_true].
  exploit (@rtc_pi_step_remove_promises tid); eauto.

  intro PI_STEPS'. des. ss.
  exploit CONSIS.
  { eauto. }
  { apply pi_steps_small_steps_snd in PI_STEPS. ss.
    eapply rtc_small_step_find in PI_STEPS; eauto.
    assert (EQ:= rtc_pi_step_except_find PI_STEPS'); des; ss.
    rewrite <-EQ0, PI_STEPS. eauto. }
  { eauto. }
  { eauto. }

  clear CONSIS. i. des.
  exploit (PI_RACEFREE cS3 ord ord0).
  { etrans.
    - eapply rtc_implies; [by i; econs; eapply H|].
      by eapply pi_steps_small_steps_fst in PI_STEPS; eauto.
    - eapply rtc_implies, STEPS. by econs; eauto.
  }
  { hexploit rtc_pi_step_future; [| |eapply rtc_implies; [eapply (@pi_step_evt_all_incl true)|]|]; eauto.
    i; des. clear FUTURES FUTURET.
    assert (LC1: exists lc1', IdentMap.find tid (Configuration.threads cS3) = Some (existT _ lang st1, lc1')).
    { erewrite <-rtc_small_step_find; eauto.
      inv WF2. rewrite THS. unfold remove_promise.
      setoid_rewrite IdentMap.Properties.F.map_o.
      destruct (IdentMap.find tid (Configuration.threads cT2)) as [[]|]; [|done].
      inv ST1. s. eauto.
    }
    des.
    econs; cycle 1.
    - econs; [by eauto|]. rdes RW; eauto.
    - eauto.
    - rdes RW; eauto.
    - eauto.
  }
  i. des. destruct ord0; inv ORD; inv ORDW.
Qed.

Lemma pi_consistent_small_step_pi_rw
      e tid cST1 cST2 cT3 withprm
      (WF: pi_wf loctmeq cST1)
      (PI_CONSISTENT: pi_consistent cST1)
      (PI_RACEFREE: pf_racefree cST1.(fst))
      (PI_STEPS: rtc (pi_step_evt true tid) cST1 cST2)
      (STEP: small_step withprm tid e cST2.(snd) cT3)
      (PRCONS: forall tid0, promise_consistent_th tid0 cT3):
  forall loc from to val rel ord tid' ts
    (NEQ: tid <> tid')
    (RW: ThreadEvent.is_reading e = Some (loc, to, val, rel, ord) \/
         ThreadEvent.is_writing e = Some (loc, from, to, val, rel, ord)),
  ~Threads.is_promised tid' loc ts cST2.(snd).(Configuration.threads).
Proof.
  ii. guardH RW.
  eapply pi_consistent_lang_step_pi_rw; eauto.
  - hexploit rtc_pi_step_future; [| |eapply rtc_implies; [eapply (@pi_step_evt_all_incl true)|]|]; eauto.
    i; des. clear FUTURES FUTURET. inv WF2.
    eauto using promise_consistent_th_small_step_backward.
  - inv STEP. inv STEP0; inv STEP; [by rdes RW; inv RW|].
    econs; eauto.
    + by rewrite TID.
    + destruct e0; rdes RW; inv RW; s; eauto.
Qed.

Lemma pi_consistent_small_step_pi
      e tid cST1 cST2 cT3 withprm
      (WF: pi_wf loctmeq cST1)
      (PI_CONSISTENT: pi_consistent cST1)
      (PI_RACEFREE: pf_racefree cST1.(fst))
      (PI_STEPS: rtc (pi_step_evt true tid) cST1 cST2)
      (STEP: small_step withprm tid e cST2.(snd) cT3)
      (FULFILL: promise_consistent_th tid cT3)
      (PRCONSIS: forall tid0, promise_consistent_th tid0 cST1.(snd)):
  exists cS3, pi_step withprm tid e cST2 (cS3,cT3).
Proof.
  destruct cST1 as [cS1 cT1], cST2 as [cS2 cT2].
  exploit rtc_pi_step_future; [eauto|reflexivity|..].
  { eapply rtc_implies, PI_STEPS. eauto. }
  intros [WF2 _].

  hexploit (promise_consistent_th_rtc_small_step).
  { econs 2; [|reflexivity]. eauto. }
  { inv WF2. eauto. }
  { eauto. }
  intro PCONSIS.

  assert (PRCONSIS3: forall tid0, promise_consistent_th tid0 cT3).
  { i. ss. eapply promise_consistent_th_small_step_forward; eauto; cycle 1.
    { inv WF2; eauto. }
    i. hexploit rtc_promise_consistent_th_small_step_forward.
    { eapply pi_steps_small_steps_snd in PI_STEPS. eauto. }
    { eauto. }
    { eapply promise_consistent_th_small_step; eauto.
      inv WF2; eauto. }
    { inv WF. eauto. }
    eauto.
  }

  assert (RW:= pi_consistent_small_step_pi_rw WF PI_CONSISTENT PI_RACEFREE PI_STEPS STEP PRCONSIS3).

  exploit rtc_pi_step_future; [| |eapply rtc_implies; [eapply pi_step_evt_all_incl|]|]; eauto.
  i; des. destruct cS2. inv WF2. ss. assert (MSTEP:=STEP). inv STEP. inv STEP0.
  - eexists. econs; [by eauto|by inv STEP; s; eauto|..].
    + inv STEP. ss. rewrite IdentMap.gss.
      setoid_rewrite IdentMap.Properties.F.map_o.
      by rewrite TID.
    + i. des; eapply (@pi_consistent_small_step_pi_rw _ _ _ (_,_)); s; try apply MSTEP; try apply PI_CONSISTENT; eauto.
  - inv STEP. inv LOCAL.
    { eexists. econs.
      - eauto.
      - econs.
        + ss. setoid_rewrite IdentMap.Properties.F.map_o.
          by rewrite TID.
        + econs 2. econs; [|econs 1]; eauto.
        + eauto.
        + eauto.
      - s. by rewrite !IdentMap.gss.
      - i. des; eapply (@pi_consistent_small_step_pi_rw _ _ _ (_,_)); s; try apply MSTEP; try apply PI_CONSISTENT; eauto.
    }
    { inv LOCAL0. eexists. econs.
      - econs; eauto. econs 2. econs; [|econs 2]; eauto. econs; eauto.
      - econs.
        + ss. setoid_rewrite IdentMap.Properties.F.map_o.
          by rewrite TID.
        + econs 2. econs; [|econs 2]; eauto.
          econs; eauto.
          s. hexploit RL; [| |by intro X; des; unfold loctmeq in *; subst; apply X]; eauto.
          i. destruct (Ident.eq_dec tid tid0) eqn: EQ; cycle 1.
          { eapply RW; s; eauto. }
          subst. intro PROMISED. inv PROMISED.
          ss. rewrite TID0 in TID. depdes TID.
          rdes FULFILL. ss. rewrite IdentMap.gss in FULFILL.
          exploit FULFILL; s; eauto.
          intro LT. ss.
          inv READABLE; eauto.
          apply TimeFacts.join_lt_des in LT. des.
          apply TimeFacts.join_lt_des in AC. des.
          revert BC0. unfold View.singleton_ur_if. condtac; ss.
          * unfold TimeMap.singleton, LocFun.add. condtac; [|congr]. i.
            eapply Time.lt_strorder. eauto.
          * unfold TimeMap.singleton, LocFun.add. condtac; [|congr]. i.
            eapply Time.lt_strorder. eauto.
        + eauto.
        + eauto.
      - s. by rewrite !IdentMap.gss.
      - i. des; eapply (@pi_consistent_small_step_pi_rw _ _ _ (_,_)); s; try apply MSTEP; try apply PI_CONSISTENT; eauto.
    }
    { destruct lc1, lc2. exploit local_simul_write; [| |by eapply LOCAL0|..].
      { instantiate (1:= memory). ii. eapply LR in IN.
        des; eauto. }
      { econs. i. destruct msg1. exploit LR; eauto. i. des.
        inv WFT. inv WF1. exploit THREADS; eauto. i. inv x. ss.
        exploit PROMISES; eauto. i.
        destruct (Time.eq_dec to1 to2); cycle 1.
        { destruct (Configuration.memory cT2 loc0).(Cell.WF). splits.
          - eapply DISJOINT0; eauto.
          - ii. inv H. congr.
        }
        subst. exfalso. eapply NOT. econs; eauto.
      }
      intro WRITE; des.
      eexists; econs.
      - eauto.
      - s. econs; s; eauto.
        + setoid_rewrite IdentMap.Properties.F.map_o. by rewrite TID.
        + rewrite Bool.orb_true_r. econs 2. econs; [|econs 3]; eauto.
      - s. by rewrite !IdentMap.gss.
      - i. des; eapply (@pi_consistent_small_step_pi_rw _ _ _ (_,_)); s; try apply MSTEP; try apply PI_CONSISTENT; eauto.
    }
    { destruct lc2, lc3. exploit local_simul_write; [| |by eapply LOCAL2|..].
      { instantiate (1:= memory). ii. eapply LR in IN.
        des; eauto. }
      { inv LOCAL1. ss.
        econs. i. destruct msg1. exploit LR; eauto. i. des.
        inv WFT. inv WF1. exploit THREADS; eauto. i. inv x.
        exploit PROMISES; eauto. i.
        destruct (Time.eq_dec to1 to2); cycle 1.
        { destruct (Configuration.memory cT2 loc0).(Cell.WF). splits.
          - eapply DISJOINT0; eauto.
          - ii. inv H. congr.
        }
        subst. exfalso. eapply NOT. econs; eauto.
      }
      intro WRITE; des.

      inv LOCAL1. eexists. econs.
      - econs; eauto. econs 2. econs; [|econs 4]; eauto; econs; eauto.
      - s. econs.
        + ss. setoid_rewrite IdentMap.Properties.F.map_o.
          by rewrite TID.
        + econs 2. econs; [|econs 4]; [by eauto|..].
          {
            econs; eauto.
            s. hexploit RL; [| |by intro X; des; unfold loctmeq in *; subst; apply X]; eauto.
            i. destruct (Ident.eq_dec tid tid0) eqn: EQ; cycle 1.
            { eapply RW; s; eauto. }
            subst. intro PROMISED. inv PROMISED.
            ss. rewrite TID0 in TID. depdes TID.

            r in FULFILL. hexploit FULFILL.
            { s. rewrite IdentMap.gss. eauto. }
            clear FULFILL. intro FULFILL.

            eapply write_step_promise_consistent in FULFILL; eauto.
            exploit FULFILL; s; eauto.
            intro LT. ss.
            inv READABLE; eauto.
            apply TimeFacts.join_lt_des in LT. des.
            apply TimeFacts.join_lt_des in AC. des.
            revert BC0. unfold View.singleton_ur_if. condtac; ss.
            * unfold TimeMap.singleton, LocFun.add. condtac; [|congr]. i.
              eapply Time.lt_strorder. eauto.
            * unfold TimeMap.singleton, LocFun.add. condtac; [|congr]. i.
              eapply Time.lt_strorder. eauto.
          }
          { eauto. }
        + eauto.
        + eauto.
      - s. by rewrite !IdentMap.gss.
      - i. des; eapply (@pi_consistent_small_step_pi_rw _ _ _ (_,_)); s; try apply MSTEP; try apply PI_CONSISTENT; eauto.
    }
    { inv LOCAL0. eexists. econs.
      - econs; eauto. econs 2. econs; [|econs 5]; eauto. econs; eauto.
      - econs.
        + ss. setoid_rewrite IdentMap.Properties.F.map_o.
          by rewrite TID.
        + econs 2. econs; [|econs 5]; eauto.
          econs; eauto.
          s. i. apply Memory.bot_nonsynch.
        + eauto.
        + eauto.
      - s. by rewrite !IdentMap.gss.
      - i. des; eapply (@pi_consistent_small_step_pi_rw _ _ _ (_,_)); s; try apply MSTEP; try apply PI_CONSISTENT; eauto.
    }
    { inv LOCAL0. eexists. econs.
      - econs; eauto. econs 2. econs; [|econs 6]; eauto. econs; eauto.
      - econs.
        + ss. setoid_rewrite IdentMap.Properties.F.map_o.
          by rewrite TID.
        + econs 2. econs; [|econs 6]; eauto.
          econs; eauto.
          s. i. apply Memory.bot_nonsynch.
        + eauto.
        + eauto.
      - s. by rewrite !IdentMap.gss.
      - i. des; eapply (@pi_consistent_small_step_pi_rw _ _ _ (_,_)); s; try apply MSTEP; try apply PI_CONSISTENT; eauto.
    }
Grab Existential Variables.
  { exact Time.bot. }
  { exact xH. }
  { exact xH. }
  { exact xH. }
  { exact xH. }
  { exact xH. }
  { exact xH. }
  { exact xH. }
  { exact xH. }
  { exact true. }
Qed.

Lemma small_step_evt_to_true
      withprm tid cST1 cST2
      (STEP: small_step_evt withprm tid cST1 cST2):
  small_step_evt true tid cST1 cST2.
Proof.
  destruct withprm; eauto.
  inv STEP. inv USTEP.
  econs. econs; eauto.
Qed.

Lemma pi_consistent_rtc_small_step_pi
      tid cST1 cST2 withprm
      (WF: pi_wf loctmeq cST1)
      (PI_CONSISTENT: pi_consistent cST1)
      (PI_RACEFREE: pf_racefree cST1.(fst))
      (PI_STEPS: rtc (pi_step_evt true tid) cST1 cST2)
      cT3 pre
      (STEP: with_pre (small_step withprm tid) cST2.(snd) pre cT3)
      (FULFILL: forall tid0, promise_consistent_th tid0 cT3):
  exists cS3 pre', with_pre (pi_step withprm tid) cST2 pre' (cS3,cT3) /\
                   pre = pi_pre_proj pre'.
Proof.
  destruct cST2 as [cS2 cT2].
  revert_until STEP. induction STEP.
  { s; i. eauto. }
  s; i.

  exploit IHSTEP; s; eauto.
  { eapply promise_consistent_th_small_step_backward; eauto.
    exploit rtc_pi_step_future.
    { eauto. }
    { reflexivity. }
    { eapply rtc_implies, PI_STEPS. eauto. }
    intros [WF2 _]. inv WF2.

    exploit with_pre_rtc_union; eauto.
    i. exploit rtc_small_step_future.
    { eauto. }
    { eapply rtc_implies, x0. eauto. }
    i; des; eauto.
  }

  intro STEPS. des. ss.
  eapply (@pi_consistent_small_step_pi _ _ _ (_,_)) in PSTEP; eauto; cycle 1.
  { etrans; eauto. subst.
    eapply rtc_implies; [eapply pi_step_evt_to_true|].
    eapply with_pre_rtc_union; eauto. }
  { eapply (@rtc_promise_consistent_th_small_step_backward true); try apply FULFILL.
    - etrans.
      + eapply pi_steps_small_steps_snd. eauto.
      + eapply rtc_implies; [eapply small_step_evt_to_true|].
        eapply with_pre_rtc_union; eauto.
    - inv WF. eauto.
  }
  des; esplits; eauto.
Qed.

Lemma pi_consistent_rtc_ftau_small_step_pi
      tid cST1 cST2 withprm
      (WF: pi_wf loctmeq cST1)
      (CONSISTENT: Configuration.consistent (snd cST1))
      (PI_CONSISTENT: pi_consistent cST1)
      (PI_RACEFREE: pf_racefree cST1.(fst))
      (PI_STEPS: rtc (pi_step_evt true tid) cST1 cST2)
      cT3 pre
      (STEP: with_pre (ftau (small_step withprm tid)) cST2.(snd) pre cT3)
      (FULFILL: forall tid0, promise_consistent_th tid0 cT3):
  exists cS3 pre', with_pre (ftau (pi_step withprm tid)) cST2 pre' (cS3,cT3) /\
                   pre = pi_pre_proj pre'.
Proof.
  destruct cST2 as [cS2 cT2].
  revert_until STEP. induction STEP.
  { s; i. eauto. }
  s; i. inv PSTEP.

  eapply with_pre_implies in STEP; cycle 1.
  { i. inv STEP0. eauto. }

  assert (WF2 : Configuration.wf ms).
  { exploit rtc_pi_step_future.
    { eauto. }
    { reflexivity. }
    { eapply rtc_implies, PI_STEPS. eauto. }
    intros [WF2 _]. inv WF2.

    exploit with_pre_rtc_union; eauto.
    i. exploit rtc_small_step_future.
    { eauto. }
    { eapply rtc_implies, x0. eauto. }
    i; des; eauto.
  }

  exploit IHSTEP; s; eauto.
  { exploit rtc_pi_step_future; try (eapply rtc_implies, PI_STEPS); eauto.
    intro; des. inv WF0.
    eauto using promise_consistent_th_small_step_backward.
  }

  intro STEPS. des. ss.
  exploit with_pre_implies; try exact STEPS; i.
  { i. inv STEP0. eauto. }

  eapply (@pi_consistent_small_step_pi _ _ _ (_,_)) in TSTEP; eauto; cycle 1.
  { etrans; eauto. subst.
    eapply rtc_implies; [eapply pi_step_evt_to_true|].
    eapply with_pre_rtc_union; eauto. }
  { inv WF. eauto using consistent_promise_consistent_th. }
  des; esplits; eauto.
Qed.

Theorem pi_consistent_step_pi
      cST1 cT3 e tid
      (WF: pi_wf loctmeq cST1)
      (PI_CONSISTENT: pi_consistent cST1)
      (CONSISTENT: Configuration.consistent cST1.(snd))
      (PI_RACEFREE: pf_racefree cST1.(fst))
      (STEP: Configuration.step e tid cST1.(snd) cT3):
  exists cST2 cS3 te,
    <<STEPS: rtc (tau (pi_step true tid)) cST1 cST2>> /\
    <<STEP: (pi_step true tid te) cST2 (cS3,cT3)>> /\
    <<EVENT: ThreadEvent.get_event te = e>>.
Proof.
  exploit step_small_steps; eauto; [by inv WF|]. i. des. subst.
  eapply rtc_tau_with_pre in STEPS. des.
  exploit pi_consistent_rtc_ftau_small_step_pi; eauto.
  { eauto using consistent_promise_consistent_th, promise_consistent_th_small_step_backward. }
  i. des.
  exploit with_pre_rtc_tau; eauto. i. des.
  exploit pi_consistent_small_step_pi.
  5: instantiate (2 := (_, _)). 5: exact STEP0. all: eauto using consistent_promise_consistent_th.
  { eapply rtc_implies, x2. i. inv H. econs. eauto. }
  { inv WF. eauto using consistent_promise_consistent_th. }
  i. des. esplits; eauto.
Qed.

author: snu-sf

repo: promising-coq

save_path: github-repos/coq/snu-sf-promising-coq


text:
(*  File 3/4 of the proofs of Fermat's Two Squares Theorem                    *)
(*                          by G. Dubach and F. Muehlboeck, IST Austria, 2021 *)
(*                                                                            *)
(*  This proof is from:                                                       *)
(*    A. David Christopher                                                    *)
(*    A partition-theoretic proof of Fermat’s Two Squares Theorem             *)
(*    Discrete Mathematics 339 (2016), no. 4, 1410-1411.                      *)
(*                                                                            *)

From mathcomp Require Import all_ssreflect finmap.
Require Import lemmata.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section Partition_Proof.
Open Scope fset_scope.
Open Scope nat_scope.

Variable p:nat.
Variable p_prime : prime p.

Definition Ip:{fset nat} := [fsetval n in 'I_p].
Definition N4 : Type := (nat * nat) * (nat * nat).
Definition Ip4:{fset N4} := ((Ip`*`Ip)`*`(Ip`*`Ip)).
Definition involutionN4:= (@involution_on [choiceType of N4]).
Definition fixed_fsetN4:=(@fixed_fset [choiceType of N4]).
Definition involutionN4_lemma:=(@involution_lemma [choiceType of N4]).

(* Y_area is the area of a Young diagram                                      *)
Definition Y_area (yd : N4) : nat := yd.1.1*yd.1.2+yd.2.1*yd.2.2.

Definition P2p :=[fset yd:N4 | (yd \in Ip4) && ((Y_area yd ==p)&&(yd.1.1>yd.2.1))].
  Definition P2p_l :=[fset yd:N4 | (yd \in P2p) && (yd.1.2<yd.2.2)].
  Definition P2p_e :=[fset yd:N4 | (yd \in P2p) && (yd.1.2==yd.2.2)].
  Definition P2p_g :=[fset yd:N4 | (yd \in P2p) && (yd.1.2>yd.2.2)].

(* Basic properties                                                           *)

Lemma modulo_ex: p %% 4 = 1 -> exists k, p=k*4+1.
Proof.
by move => h_pmod4; exists (p%/4); rewrite{1} (divn_eq p 4) h_pmod4.
Qed.

Lemma Ip4_not_p_factors (a f : nat): a \in Ip -> f \in Ip -> ~ (a * f == p).
Proof.
move => ha hf.
apply (elimT negP).
by_contradiction hassume.
  have hda : a %| p by rewrite /dvdn -(eqnP hassume) modnMr.
  have hdf : f %| p by rewrite /dvdn -(eqnP hassume) modnMl.
  have [hp hdiv] := (primeP p_prime).
  apply hdiv in hda,hdf.
  rewrite /Ip in ha,hf.
  zag_solve.
Qed.

Lemma area_gt0_all : forall yd : N4, (yd \in Ip4) -> Y_area yd == p
-> (yd.1.1 > 0)/\(yd.1.2>0)/\(yd.2.1>0)/\(yd.2.2>0).
Proof.
move => [[a1 f1] [a2 f2]] hin harea.
rewrite !inE in hin.
rewrite /Y_area /= in harea.
destruct_boolhyp hin => /= hina1 hinf1 hina2 hinf2.
repeat split; by_contradiction hc; exfalso;
  apply (introT negPf) in hc; rewrite -leqNgt leqn0 in hc;
  rewrite (eqnP hc) in harea;
  rewrite ?mul0n ?muln0 ?add0n ?addn0 in harea;
  unshelve eapply (Ip4_not_p_factors _ _ harea); by [].
Qed.

Lemma P2p_in_Ip4 (yd:N4): (yd \in P2p)-> (yd \in Ip4).
Proof.
rewrite inE; by rewrite inE => /andP [hinI4 _].
Qed.

(* Study of P2p via conjugation                                               *)

Definition conjugate (a : N4) : N4:= ((a.1.2 + a.2.2,a.2.1),(a.1.2,a.1.1-a.2.1)).

Lemma conjugate_involution : involutionN4 P2p conjugate.
Proof.
split.
 - move => yd hin.
   have hinI4 := (@P2p_in_Ip4 yd hin).
   rewrite !inE in hin.
   destruct_boolhyp hin => hina1 hinf1 hina2 hinf2 harea hleq.
   have [ha1 [hf1 [ha2 hf2]]] := (@area_gt0_all yd hinI4 harea).
   rewrite /conjugate !inE /Y_area.
   rewrite /Y_area in harea.
   zag_solve.
 - move => [[a1 f1] [a2 f2]] hin; rewrite !inE in hin.
   destruct_boolhyp hin => hina1 hinf1 hina2 hinf2 _.
   rewrite /conjugate.
   zag_solve.
Qed.

Lemma conjugate_fixed : (modn p 4  = 1) -> #|`fixed_fsetN4 P2p conjugate| = 1.
Proof.
move /modulo_ex => [k hk].
have h_singleton : fixed_fsetN4 P2p conjugate = [fset ((2*k+1,1),(1,2*k))].
- apply/eqP; rewrite eqEfsubset; apply/andP; split;
  apply/fsubsetP => yd; rewrite !inE /conjugate; move: yd=>[[a1 f1] [a2 f2]] /= h.
  + destruct_boolhyp h => /= ha1 hf1 ha2 hf2 harea hlt heq hf1a2 ha2f1 hf2a1a2.
    mcsimpl; subst; rewrite /Y_area /= in harea.
    have harea' : a2 * (a2 + f2 + f2) == p by mcnia.
    have hdvdn := (n_dvdn harea').
    have ha2_1: a2 = 1.
    - have p_prime' := p_prime; apply (elimT primeP) in p_prime'.
      destruct p_prime' as [_ hdiv]; apply hdiv in hdvdn.
      by destruct_boolhyp hdvdn; mcnia.
    zag_solve.
  + move: h => /eqP [ha1 hf1 ha2 hf2].
    rewrite ha1 hf1 ha2 hf2 /Y_area.
    have kgt0 : k > 0.
    - by_contradiction hkgt0.
      have hk0: (k = 0) by mcnia.
      have p_prime' := p_prime; apply (elimT primeP) in p_prime'.
      mccontradiction.
    zag_solve.
rewrite h_singleton; by rewrite cardfs1.
Qed.

Lemma P2p_odd :  (modn p 4  = 1) -> odd(#|`P2p|).
Proof.
rewrite -(@involutionN4_lemma conjugate P2p conjugate_involution).
move => hp4.
by rewrite conjugate_fixed.
Qed.

(* Study of P2p_l via double transposition                                    *)

Definition transpose_l (a : N4) : N4:= ((a.2.2,a.2.1),(a.1.2,a.1.1)).

Lemma transpose_l_involution : involutionN4 P2p_l transpose_l.
Proof.
split.
 - move => [[a1 f1] [a2 f2]].
   rewrite !inE /Y_area /transpose_l.
   zag_solve.
 - move => [[a1 f1] [a2 f2]].
   rewrite !inE /transpose_l.
   zag_solve.
Qed.

Lemma transpose_l_fixed : #|`fixed_fsetN4 P2p_l transpose_l| = 0.
Proof.
have heq0 : fixed_fsetN4 P2p_l transpose_l = fset0; [|by rewrite heq0].
apply (elimT eqP).
rewrite /fixed_fsetN4 /fixed_fset -fsubset0.
by_contradiction hsubset.
apply (introT negPf) in hsubset.
apply (elimT (fsubsetPn _ _)) in hsubset.
move: hsubset => [[[a1 f1] [a2 f2]] hin _].
rewrite !inE in hin.
destruct_boolhyp hin => /= ha1 hf1 ha2 hf2 harea ha2a1 hf1f2 ha1f2 hf1a2 _ _.
rewrite /Y_area /= in harea.
mcsimpl; subst.
have p_prime' := p_prime. apply (elimT primeP) in p_prime'.
move: p_prime' => [hp1 hdvdnp].
have harea' :  2 * (a2 * f2) == p by mclia.
have h2divp := (n_dvdn harea').
apply hdvdnp in h2divp.
rewrite /= in h2divp.
have ha2_1 : a2 = 1 by mcnia.
have hf2_1 : f2 = 1 by mcnia.
by rewrite ha2_1 hf2_1 ltnn in ha2a1.
Qed.

Theorem P2p_l_even : ~~odd(#|`P2p_l|).
Proof.
rewrite -(@involutionN4_lemma transpose_l P2p_l transpose_l_involution).
by rewrite transpose_l_fixed.
Qed.

(* Study of P2p_e via enumeration                                             *)

Lemma mod4_halfeven : (modn p 4  = 1) -> (divn (p - 1) 2) %% 2 == 0.
Proof.
apply (elimT primeP) in p_prime.
move: p_prime => [hp1 hdvdn] hpmod.
have hp: (p - 1).+1 = p by mcnia.
have hp1mod : (p-1) %% 4 = 0.
- rewrite subn1 modn_pred; [|by []| auto;fail].
  by rewrite hpmod /= /dvdn hpmod /=.
by rewrite modn_divl /muln /= hp1mod div0n.
Qed.

Definition P2p_e_mapfun : nat -> N4 := fun x : nat => ((p - (x + 1), 1), (x + 1, 1)).

Lemma P2p_e_I_map : P2p_e = [fset (P2p_e_mapfun x) | x in [fsetval y in 'I_((divn (p - 1) 2))]].
Proof.
have p_prime' := p_prime.
apply (elimT primeP) in p_prime'.
move: p_prime' => [hp1 hprime].
apply /eqP.
(* unfold definitions and assert set equality by mutual subset relationship *)
rewrite /P2p_e /P2p /P2p_e_mapfun eqEfsubset.
(* both subset relationships hold because there exists no element in
   the subset that does not exist in the superset.
   both proofs eventually rely on the fact that p > 2, and therefore
   p - 1 must be even. *)
apply /andP; split;
  apply subset_by_in;
  move => [[[a1 f1] [a2 f2]] hin hnin];
  apply (elimT negP) in hnin; apply hnin; clear hnin.
  (* the first case is the easier one; the hard part is
     to prove that (a2 - 1) < floor((p - 1)/2).
     First, however, we collect some facts and prove that f1 = f2 = 1*)
- rewrite !inE /Ip /= in hin.
  destruct_boolhyp hin => /= ha1 hf1 ha2 hf2 harea ha2a1 hf1f2.
  have hgt0 := (@area_gt0_all ((a1,f1),(a2,f2)) _ harea).
  hyp_progress hgt0; [by rewrite /Ip4 !inE; zag_solve|].
  move: hgt0 => /= [ha1_0 [hf1_0 [ha2_0 hf2_0]]].
  rewrite (eqnP hf1f2) /Y_area /= in harea.
  rewrite (eqnP hf1f2).
  clear hf1f2 hf1 hf1_0 f1.
  have hf2_1 : f2 = 1.
  + replace (a1 * f2 + a2 * f2) with (f2 * (a1 + a2)) in harea; [|by ring].
    apply (n_dvdn) in harea.
    apply hprime in harea.
    zag_solve.
  rewrite hf2_1.
  rewrite hf2_1 !muln1 in harea.
  clear hf2_1 hf2 hf2_0 f2.
  (* Now it is easy to see that the way to instantiate
     x to satisfy the membership goal is by (a2 - 1), which means we
     need to prove that (a2 - 1) < (p - 1) % 2 *)
  apply /imfsetP; exists (a2 - 1); [|zag_solve].
  apply/imfsetP; unshelve (eexists (Sub (a2 - 1) _)).
  (* the following fact (relying on the knowledge that p-1 is even)
     helps mcnia figure out that the inequation holds *)
  + have hp : p - 1 = 2 * ((p - 1) %/ 2).
    - have hpgt2 : p > 2 by mcnia.
      apply (elimT eqP).
      rewrite mulnC eq_sym -dvdn_eq dvdn2 -oddS subn1 -Lt.S_pred_pos; [|by mcsolve].
      apply even_prime in p_prime.
      case p_prime; zag_solve.
    mcnia.
  + zag_solve.
  + zag_solve.
  (* the second part is the more complicated one; it again
     relies on the fact that p > 2 and therefore odd.
     This in turn means that we can prove the inequality
     2 * (x + 1) < p by weakening the inequality to <=
     and proving that the equal-case cannot hold as the LHS
     is even, but p is odd.
     *)
- rewrite !inE /=.
  apply (elimT (imfsetP _ _ _ _)) in hin.
  move: hin => [x hin heq].
  inversion heq; subst; clear heq.
  rewrite in_Imfset_eq in hin.
  have hxp : 2 * x < (p - 2).
  + have hpgt2 : p > 2.
    - by_contradiction hcontra.
      have hp2: p = 2 by mclia.
      mccontradiction.
    have pdiv2 : 2 %| (p - 1).
    - apply even_prime in p_prime.
      rewrite dvdn2 oddB; zag_solve.
      destruct p_prime as [hp|hp]; try rewrite hp; zag_solve.
    rewrite ltn_subRL.
    replace (2 + 2 * x) with (2 * (x + 1)); [|by mclia].
    (* now turn < into != && <= *)
    rewrite ltn_neqAle.
    apply /andP; split.
    (* != holds because even != odd *)
    - by_contradiction hcontra.
      rewrite dvdn2 -oddS subn1 -Lt.S_pred_pos -(eqP hcontra) in pdiv2; [|by mclia].
      by rewrite oddM /= in pdiv2.
    (* <= holds by hin and p-1's evenness *)
    - rewrite ltn_divRL in hin; zag_solve.
  (* the fact that 2 * x < (p - 2) suffices to solve the rest *)
  rewrite /Y_area; zag_solve.
Qed.

Lemma Pdp_e_card_pairs : #|`P2p_e| = (divn (p - 1) 2).
Proof.
rewrite P2p_e_I_map !card_imfset /=.
- by rewrite -cardE card_ord.
- rewrite /injective => x1 x2 h.
  by apply ord_inj in h.
- move => x1 x2 h.
  apply /eqP.
  by_contradiction heq.
  rewrite /P2p_e_mapfun in h.
  apply (introT eqP) in h.
  rewrite !xpair_eqE in h.
  have hx1x2 : x1 == x2 by zag_solve.
  mccontradiction.
Qed.

Lemma Pdp_e_card :  (modn p 4  = 1) -> ~~odd(#|`P2p_e|).
Proof.
move => hmod.
rewrite Pdp_e_card_pairs.
apply mod4_halfeven in hmod.
by rewrite -eqb0 -modn2.
Qed.

Lemma card_disjoint_triple {K : choiceType} (A B C : {fset K}) :
A `&` B = fset0 -> A `&` C = fset0 -> B `&` C = fset0
-> #|` A `|` B `|` C | = #|` A | + #|` B | + #|` C |.
Proof.
move => hab hac hbc.
have hui1 := (cardfsUI (A `|` B) C).
have hui2 := (cardfsUI A B).
rewrite hab cardfs0 addn0 in hui2.
rewrite hui2 in hui1.
by rewrite -hui1 fsetIUl hac hbc fsetU0 cardfs0 addn0.
Qed.

Lemma P2p_partition: #|`P2p|=#|`P2p_l|+#|`P2p_e|+#|`P2p_g|.
Proof.
have hunion : P2p = P2p_l `|` P2p_e `|` P2p_g.
- apply /eqP.
  rewrite eqEfsubset.
  apply /andP; split; apply subset_by_in; move => [[[a1 f1] [a2 f2]] hin hnin].
  + rewrite !inE /= in hin.
    rewrite !in_fsetU !Bool.negb_orb !inE !Bool.negb_andb /= in hnin.
    destruct_boolhyp hin => /= ha1 hf1 ha2 hf2 harea ha2a1.
    destruct_boolhyp hnin; try mccontradiction; move => hx1 hx2 hx3.
    rewrite -leqNgt leq_eqVlt in hx1.
    zag_solve.
  + rewrite !inE !Bool.negb_andb /= in hnin.
    rewrite !in_fsetU !inE /= in hin.
    destruct_boolhyp hin => /= ha1 hf1 ha2 hf2 harea ha2a1;
    destruct_boolhyp hnin; mccontradiction.
- rewrite hunion.
  by apply card_disjoint_triple;
    apply (elimT eqP); rewrite fsetI_eq0; apply /fdisjointP;
    move => [[a1 f1] [a2 f2]] hin; rewrite !inE /Y_area /= in hin;
    rewrite !inE /Y_area /=; apply (introT negP); move => hnin;
    destruct_boolhyp hin; destruct_boolhyp hnin; intros; mccontradiction.
Qed.

Lemma P2p_g_odd : (modn p 4  = 1) -> odd #|` P2p_g |.
move => hmod.
have hodd := P2p_odd hmod.
rewrite P2p_partition !oddD in hodd.
by rewrite (negPf P2p_l_even) (negPf (Pdp_e_card hmod)) /= in hodd.
Qed.

(* Study of P2p_g via simple transposition                                    *)

Definition transpose_g (a : N4) : N4:= ((a.1.2,a.1.1),(a.2.2,a.2.1)).

Lemma transpose_g_involution : involutionN4 P2p_g transpose_g.
Proof.
split.
- move => yd hin; rewrite !inE /Y_area in hin.
  rewrite /transpose_l !inE /Y_area.
  zag_solve.
- move => [[a1 f1] [a2 f2]] hin; rewrite !inE /Y_area in hin.
  rewrite /transpose_g.
  zag_solve.
Qed.

Lemma transpose_g_fixed : (exists (yd:N4), (yd \in (fixed_fsetN4 P2p_g transpose_g)))
                                 -> (exists a b :nat, p=a^2 + b^2).
Proof.
move => [[[a1 f1] [a2 f2]] hin] /=.
exists a1; exists a2.
rewrite !inE /transpose_g /Y_area /= in hin.
destruct_boolhyp hin => /=; intros.
mcnia.
Qed.

(*                                                                            *)
(* Proof of Fermat's theorem using partitions, following David Christopher    *)
(*                                                                            *)

Theorem Fermat_David_Christopher : p %% 4 = 1 -> exists a b :nat, p=a^2 + b^2.
Proof.
move => hk.
apply transpose_g_fixed.
apply odd_existence.
rewrite involution_lemma.
- by apply P2p_g_odd.
- by apply transpose_g_involution.
Qed.

End Partition_Proof.

author: gdubach


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

Definition table_T (tuple_T: Type) := list tuple_T.
Definition non_empty {tuple_T: Type} (l: table_T tuple_T) :=
  match l with
   | nil => False
   | h :: t => True
  end.

Fixpoint sorted {tuple_T: Type}
(cmp: tuple_T->tuple_T-> bool) (t: table_T tuple_T) :=
  match t with
    | nil => True
    | h :: t => (match t with
        | nil => True
        | h1 :: t1 => if cmp h h1 then (sorted cmp t) else False
        end )
  end.

Lemma sorted_helper {tuple_T: Type} :
forall (cmp: tuple_T->tuple_T-> bool) (t: table_T tuple_T) (a: tuple_T),
sorted cmp (a::t) -> sorted cmp t.
Proof.
Admitted.

Fixpoint filter {tuple_T: Type}
(f : tuple_T -> bool) (l : table_T tuple_T) : table_T tuple_T:=
  match l with
  | nil => nil
  | h :: t => if f h then h :: (filter f t) else (filter f t)
  end.

Fixpoint last_in_sorted {tuple_T: Type}
(cmp: tuple_T->tuple_T-> bool) (default: tuple_T) (t: table_T tuple_T) : tuple_T :=
  match t with
    | nil => default
    | h :: t1 => if cmp h (last_in_sorted cmp default t1)
                then (last_in_sorted cmp default t1) else h
  end.

Definition last_in_sorted2 {tuple_T: Type}
(cmp: tuple_T->tuple_T-> bool) (default: tuple_T) (t: table_T tuple_T) : tuple_T :=
  match t with
    | nil => default
    | h :: t1 => h
  end.

(* Fixpoint topK {tuple_T: Type}
  (t: table_T tuple_T) (K: nat) : table_T tuple_T :=
  match t with
    | nil => nil
    | h :: t1 => match K with
      | O => nil
      | S k1 => h:: (topK t1 k1)
      end
  end.
*)

Definition cmp_transitive {tuple_T: Type} (cmp: tuple_T->tuple_T->bool) :=
forall (a b c: tuple_T) ,
  cmp a b = true /\ cmp b c = true -> cmp a c = true.

Fixpoint lt_nat (n m : nat) : bool :=
  match n with
  | O => match m with
      | O => false
      | S m' => true
      end
  | S n' =>
      match m with
      | O => false
      | S m' => lt_nat n' m'
      end
  end.

Fixpoint gt_nat (n m : nat) : bool :=
  match n with
  | O => false
  | S n' =>
      match m with
      | O => true
      | S m' => gt_nat n' m'
      end
  end.

Notation "x <? y" := (lt_nat x y).
Notation "x >? y" := (gt_nat x y) (at level 70).
Lemma lt_rewrite_true :
forall (n m : nat), n <? m = true <-> n < m.
Proof.
Admitted.

Lemma lt_rewrite_false :
forall (n m : nat), n <? m = false <-> n >= m.
Proof.
Admitted.

Lemma gt_rewrite_true :
forall (n m : nat), n >? m = true <-> n > m.
Proof.
Admitted.

Lemma gt_rewrite_false :
forall (n m : nat), n >? m = false <-> n <= m.
Proof.
Admitted.

Fixpoint topK {tuple_T: Type}
  (t: table_T tuple_T) (K: nat) : table_T tuple_T :=
  match t with
    | nil => nil
    | h :: t1 => if ((length t1) <? K) then h::t1 else topK t1 K
  end.

Lemma topK_remove_element {tuple_T: Type}:
forall (a: tuple_T) (t: table_T tuple_T) (K: nat),
  length t >= K -> topK t K = topK (a::t) K.
Proof.
Admitted.

Lemma topK_length_cap {tuple_T: Type}:
forall (t: table_T tuple_T) (K: nat),
  length (topK t K) <= K.
Proof.
intros. induction t. simpl. apply Nat.le_0_l.
simpl. case (length t <? K) eqn:Hx.
apply lt_rewrite_true in Hx. simpl. apply lt_le_S. auto.
auto.
Qed.

Lemma topK_sorted {tuple_T: Type}:
forall (t: table_T tuple_T) (K: nat) (cmp: tuple_T->tuple_T->bool),
  sorted cmp t -> sorted cmp (topK t K).
Proof.
intros. induction t. auto.
simpl. case (length t <? K) eqn:Hx.
apply lt_rewrite_true in Hx. auto.
apply IHt. apply sorted_helper in H. auto.
Qed.

Lemma topK_reapply {tuple_T: Type}:
  forall (t: table_T tuple_T) (K: nat),
  topK t K = topK (topK t K) K.
Proof.
intros. induction t. auto.
simpl. case (length t <? K) eqn:Hx.
simpl. rewrite Hx. auto.
apply IHt.
Qed.

(* the first (cmp r default = true) can be ignored as the default value
  is only used when the table is empty *)
Lemma topK_sorted_cmp {tuple_T: Type}:
  forall (K: nat) (cmp: tuple_T->tuple_T->bool) (t: table_T tuple_T) (r default: tuple_T),
  (cmp r default = true) /\ (cmp_transitive cmp) /\
  (sorted cmp t) /\ (cmp r (last_in_sorted2 cmp default t) = true) ->
    cmp r (last_in_sorted2 cmp default (topK t K)) = true.
Proof.
intros.
destruct H as [H0 H1].
destruct H1 as [H1 H2].
destruct H2 as [H2 H3].
unfold last_in_sorted2.
induction t. auto.
simpl.
case (length t <? K) eqn:Hx.
{ (* (length t <? K) = true *)
  auto. }
{ (* (length t <? K) = false *)
  destruct t as [|e t2] . simpl. auto.
  apply IHt. apply sorted_helper with (a). auto.
  simpl.
  simpl in H3.
  assert (cmp_helper: cmp a e = true).
  { unfold sorted in H2. case (cmp a e) eqn:contra.
    auto. auto. }
  unfold cmp_transitive in H1.
  apply H1 with (a). auto.
}
Qed.

Definition max_default {tuple_T: Type} (cmp: tuple_T->tuple_T->bool) (default: tuple_T) :=
  forall (r: tuple_T), cmp r default = true.

(* pre-condition 1 *)
(* |F(topK (T))| < K -> (forall r, r <= min(T) -> G(r) = empty). *)
Definition topK_precond {tuple_T: Type} (K: nat) (f g: tuple_T->bool)
(cmp: tuple_T->tuple_T-> bool):=
forall (default: tuple_T) (t: table_T tuple_T),
(max_default cmp default /\ sorted cmp t /\ length (filter f (topK t K)) < K ) ->
  (forall (r: tuple_T), cmp r (last_in_sorted2 cmp default t) = true -> (g r = false)).

Definition topK_precond_with_length {tuple_T: Type} (len K: nat) (f g: tuple_T->bool)
(cmp: tuple_T->tuple_T-> bool):=
forall (default: tuple_T) (t: table_T tuple_T),
(length t <= len /\ max_default cmp default /\ sorted cmp t /\ length (filter f (topK t K)) < K ) ->
  (forall (r: tuple_T), cmp r (last_in_sorted2 cmp default t) = true -> (g r = false)).

Theorem topK_precond_smp :
forall (tuple_T: Type) (K: nat) (cmp: tuple_T->tuple_T-> bool) (f g: tuple_T->bool),
  (cmp_transitive cmp) /\
  (topK_precond_with_length (S K) K f g cmp) ->
  topK_precond K f g cmp.
Proof.
intros.
unfold topK_precond.
intros.
destruct H as [H4 H5].
destruct H0 as [H0 H2].
destruct H2 as [H2 H3].
case (length t >? S K) eqn:Hx.
(* (length t >? S K) = true *)
{
  unfold topK_precond_with_length in H5.
  apply H5 with (default) (topK t K).
  split. rewrite topK_length_cap. auto.
  split. auto.
  split. apply topK_sorted. auto.
  rewrite <- topK_reapply. auto.
  apply topK_sorted_cmp.
  split. auto.
  split. auto.
  split.  auto. auto.
}
(* (length t >? S K) = false *)
{
  unfold topK_precond_with_length in H5.
  apply H5 with (default) (t).
  split. apply gt_rewrite_false in Hx. auto.
  split. auto.
  split. auto. auto.
  auto.
}
Qed.

Theorem topK_smp :
forall (tuple_T: Type) (K: nat) (cmp: tuple_T->tuple_T-> bool) (f g: tuple_T->bool) (default: tuple_T),
(
  (topK_precond K f g cmp) /\ (max_default cmp default) /\
  (forall (t: table_T tuple_T),
    ((length t)<= S K /\ (sorted cmp t)) -> filter f (topK t K) = topK (filter g t) K)
->(forall (t: table_T tuple_T),
    ((length t)> S K /\ (sorted cmp t)) -> filter f (topK t K) = topK (filter g t) K)
).
Proof.
intros.
destruct H0 as [H0 H1].
destruct H as [H H2].
destruct H2 as [H2 H3].
induction t. simpl. reflexivity.
simpl.
assert (length_t1: length t <? K = false).
  { apply lt_rewrite_false. simpl in H0. apply gt_S_n in H0. }
rewrite length_t1.
case (length (filter f (topK t K)) <? K) eqn:topK_len.
(* |F(topK(t))| < K *)
{
  assert (g a = false).
    { unfold topK_precond in H. apply H with default t.
      split. auto.
      split. apply sorted_helper in H1. auto.
      rewrite lt_rewrite_true in topK_len. auto.
      destruct t. simpl. auto.
      simpl. simpl in H1.
      case (cmp a t) eqn:cmp_a_t.
      auto. auto.
    }
  rewrite H4.
  case (length t >? S K) eqn:length_split.
  { apply IHt. rewrite gt_rewrite_true in length_split. auto.
    apply sorted_helper with (a). auto.
  }
  { apply H3. split. rewrite gt_rewrite_false in length_split. auto.
    apply sorted_helper with (a). auto.
  }
}
(* |F(topK(t))| = K *)
{
  rewrite lt_rewrite_false in topK_len.
  rewrite lt_rewrite_false in length_t1.
  assert (filter f (topK t K) = topK (filter g t) K).
    { case (length t >? S K) eqn:topK_fit.
      (* (length t >? S K) = true *)
       { apply gt_rewrite_true in topK_fit.
         apply IHt. auto. auto. apply sorted_helper with (a). auto. }
      (* (length t >? S K) = false *)
       { apply gt_rewrite_false in topK_fit.
         apply H3. split. auto. auto. apply sorted_helper with (a). auto. }
    }
  assert (length (filter g t) >= K).
    { rewrite H4 in topK_len.  }
  rewrite H4.
  case (g a) eqn:g_a.
    { (* g a = true *)
      assert (a :: filter g t = filter g (a::t)).
        { simpl. rewrite g_a. auto. }
      apply topK_remove_element. auto.
    }
    { (* g a = false *) auto. }
}
Qed.

author: predicate-udf

repo: pushdown-smp-proof


text:
Require Import Platform.tests.Thread0.

Module Make(M : S).
Import M.

Module T := Thread0.Make(M).
Import T.

Definition handlerS := SPEC reserving 49
  Al fs, PREmain[_] sched fs * mallocHeap 0.

Definition mainS := SPEC reserving 49
  PREmain[_] M.globalSched =?> 1 * mallocHeap 0.

Definition m := bimport [[ "scheduler"!"init" @ [initS], "scheduler"!"exit" @ [exitS],
                           "scheduler"!"spawn" @ [spawnS], "scheduler"!"yield" @ [yieldS] ]]
  bmodule "test" {{
    bfunctionNoRet "handler"("x", "y") [handlerS]
      Yield
      [Al fs, PREmain[_] sched fs * mallocHeap 0];;
      Exit 50
    end with bfunctionNoRet "main"("x", "y") [mainS]
      Init
      [Al fs, PREmain[_] sched fs * mallocHeap 0];;

      Spawn("test"!"handler", 50)
      [Al fs, PREmain[_] sched fs * mallocHeap 0];;

      Exit 50
    end
  }}.

Theorem ok : moduleOk m.
  vcgen; abstract (sep_auto; auto).
Qed.

End Make.

author: JasonGross


text:
Require Coq.Arith.Compare_dec.

Require Import Coq.Structures.OrderedType.
Require Import Coq.Structures.OrderedTypeEx.
Require Import Coq.FSets.FMapAVL.
Require Import Coq.FSets.FSetAVL.
Require Import Coq.Arith.Peano_dec.
Require Import Omega.

Require Import Aniceto.Map.

Require Coq.FSets.FMapFacts.

Inductive tid := taskid : nat -> tid.

Definition tid_nat r := match r with | taskid n => n end.

Definition tid_first := taskid 0.

Definition tid_next m := taskid (S (tid_nat m)).

Module TID <: UsualOrderedType.
  Definition t := tid.
  Definition eq := @eq tid.
  Definition lt x y := lt (tid_nat x) (tid_nat y).
  Definition eq_refl := @eq_refl t.
  Definition eq_sym := @eq_sym t.
  Definition eq_trans := @eq_trans t.
  Lemma lt_trans: forall x y z : t, lt x y -> lt y z -> lt x z.
  Proof.
    intros.
    unfold lt in *.
    destruct x, y, z.
    simpl in *.
    omega.
  Qed.

  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
  Proof.
    unfold lt in *.
    intros.
    destruct x, y.
    simpl in *.
    unfold not; intros.
    inversion H0.
    subst.
    apply Lt.lt_irrefl in H.
    inversion H.
  Qed.

  Import Coq.Arith.Compare_dec.
  Lemma compare:
    forall x y, Compare lt eq x y.
  Proof.
    intros.
    destruct x, y.
    destruct (Nat_as_OT.compare n n0);
    eauto using LT, GT.
    apply EQ.
    unfold Nat_as_OT.eq in *.
    subst.
    intuition.
  Defined.

  Lemma eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
  Proof.
    intros.
    unfold eq.
    destruct x, y.
    destruct (eq_nat_dec n n0).
    - subst; eauto.
    - right.
      unfold not.
      intros.
      contradiction n1.
      inversion H; auto.
  Defined.
End TID.

Module MT := FMapAVL.Make TID.
Module MT_Facts := FMapFacts.Facts MT.
Module MT_Props := FMapFacts.Properties MT.
Module MT_Extra := MapUtil MT.
Module ST := FSetAVL.Make TID.
Definition set_tid := ST.t.

Lemma tid_eq_rw:
  forall (k k':tid), TID.eq k k' <-> k = k'.
Proof.
  intros.
  auto with *.
Qed.

Lemma tid_eq_dec:
  forall x y : tid, {x = y} + {x <> y}.
Proof.
  auto using tid_eq_rw, TID.eq_dec.
Defined.

Section NotIn.
  Variable elt:Type.

  Let lt_irrefl:
    forall x : tid, ~ TID.lt x x.
  Proof.
    unfold not; intros.
    apply TID.lt_not_eq in H.
    contradiction H.
    apply TID.eq_refl.
  Qed.

  Let lt_next:
    forall x, TID.lt x (tid_next x).
  Proof.
    intros.
    destruct x.
    unfold tid_next, tid_nat, TID.lt.
    simpl.
    auto.
  Qed.

  Let tid_impl_eq:
    forall k k' : tid, k = k' -> k = k'.
  Proof.
    auto.
  Qed.

  Definition supremum {elt:Type} := @MT_Extra.supremum elt tid_first tid_next TID.lt TID.compare.

  Theorem find_not_in:
    forall (m: MT.t elt),
    ~ MT.In (supremum m) m.
  Proof.
    intros.
    eauto using MT_Extra.find_not_in, TID.lt_trans.
  Qed.

End NotIn.

author: cogumbreiro

repo: gorn-coq

save_path: github-repos/coq/cogumbreiro-gorn-coq


text:
From Hammer Require Import Hammer.

Require Import Bool Arith ZArith String.
Require ClassicalFacts.
Require Export ClassicalDescription FunctionalExtensionality.

Open Scope bool_scope.
Open Scope list_scope.

Set Implicit Arguments.
Unset Strict Implicit.

Create HintDb hahn discriminated.
Create HintDb hahn_refl discriminated.
Create HintDb hahn_full discriminated.

Ltac exten := apply functional_extensionality.

Coercion is_true (b : bool) : Prop := b = true.

Lemma hahn__true_is_true : true.
Proof. hammer_hook "HahnBase" "HahnBase.hahn__true_is_true". reflexivity. Qed.

Lemma hahn__not_false_is_true : ~ false.
Proof. hammer_hook "HahnBase" "HahnBase.hahn__not_false_is_true". discriminate. Qed.

Hint Resolve hahn__true_is_true hahn__not_false_is_true.

Ltac hahn__basic_done :=
solve [trivial with hahn | simple apply sym_equal; trivial | discriminate | contradiction].

Ltac done := trivial with hahn; hnf; intros;
solve [try hahn__basic_done; split;
try hahn__basic_done; split;
try hahn__basic_done; split;
try hahn__basic_done; split;
try hahn__basic_done; split; hahn__basic_done
| match goal with H : ~ _ |- _ => solve [case H; trivial] end].

Ltac edone := try eassumption; trivial; hnf; intros;
solve [try eassumption; try hahn__basic_done; split;
try eassumption; try hahn__basic_done; split;
try eassumption; try hahn__basic_done; split;
try eassumption; try hahn__basic_done; split;
try eassumption; try hahn__basic_done; split;
try eassumption; hahn__basic_done
| match goal with H : ~ _ |- _ => solve [case H; trivial] end].

Tactic Notation "by"  tactic(tac) := (tac; done).
Tactic Notation "eby" tactic(tac) := (tac; edone).

Module Equality.

Definition axiom T (e : T -> T -> bool) :=
forall x y, reflect (x = y) (e x y).

Structure mixin_of T := Mixin {op : T -> T -> bool; _ : axiom op}.
Notation class_of := mixin_of (only parsing).

Section ClassDef.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.

Definition class cT' :=
match cT' return class_of (sort cT') with @Pack _ c _ => c end.

Definition pack (T: Type) c := @Pack T c T.

End ClassDef.

Module Exports.
Coercion sort : type >-> Sortclass.
Notation eqType := type.
Notation EqMixin := Mixin.
Notation EqType T m := (@pack T m).
End Exports.

End Equality.
Export Equality.Exports.

Definition eq_op T := Equality.op (Equality.class T).
Arguments eq_op {T}.

Lemma eqE : forall T x, eq_op x = Equality.op (Equality.class T) x.
Proof. hammer_hook "HahnBase" "HahnBase.eqE". done. Qed.

Lemma eqP : forall T, Equality.axiom (@eq_op T).
Proof. hammer_hook "HahnBase" "HahnBase.eqP". by unfold eq_op; destruct T as [? []]. Qed.
Arguments eqP [T] x y.

Lemma hahn__internal_eqP :
forall (T: eqType) (x y : T), reflect (x = y) (eq_op x y).
Proof. hammer_hook "HahnBase" "HahnBase.hahn__internal_eqP". apply eqP. Qed.

Lemma neqP : forall (T: eqType) (x y: T), reflect (x <> y) (negb (eq_op x y)).
Proof. hammer_hook "HahnBase" "HahnBase.neqP". intros; case eqP; constructor; auto. Qed.

Lemma beq_refl : forall (T : eqType) (x : T), eq_op x x.
Proof. hammer_hook "HahnBase" "HahnBase.beq_refl". by intros; case eqP. Qed.

Lemma beq_sym : forall (T : eqType) (x y : T), (eq_op x y) = (eq_op y x).
Proof. hammer_hook "HahnBase" "HahnBase.beq_sym". intros; do 2 case eqP; congruence. Qed.

Hint Resolve beq_refl : hahn.
Hint Rewrite beq_refl : hahn_trivial.

Notation eqxx := beq_refl.

Fixpoint eqn_rec (x y: nat) {struct x} :=
match x, y with
| O, O => true
| S x, S y => eqn_rec x y
| _, _ => false
end.

Definition eqn := match tt with tt => eqn_rec end.

Lemma eqnP: forall x y, reflect (x = y) (eqn x y).
Proof. hammer_hook "HahnBase" "HahnBase.eqnP".
induction x; destruct y; try (constructor; done).
change (eqn (S x) (S y)) with (eqn x y).
case IHx; constructor; congruence.
Qed.

Canonical Structure nat_eqMixin := EqMixin eqnP.
Canonical Structure nat_eqType := Eval hnf in EqType nat nat_eqMixin.

Lemma eqnE : eqn = (@eq_op _).
Proof. hammer_hook "HahnBase" "HahnBase.eqnE". done. Qed.

Lemma hahn__negb_rewrite : forall b, negb b -> b = false.
Proof. hammer_hook "HahnBase" "HahnBase.hahn__negb_rewrite". by intros []. Qed.

Lemma hahn__andb_split : forall b1 b2, b1 && b2 -> b1 /\ b2.
Proof. hammer_hook "HahnBase" "HahnBase.hahn__andb_split". by intros [] []. Qed.

Lemma hahn__nandb_split : forall b1 b2, b1 && b2 = false -> b1 = false \/ b2 = false.
Proof. hammer_hook "HahnBase" "HahnBase.hahn__nandb_split". intros [] []; auto. Qed.

Lemma hahn__orb_split : forall b1 b2, b1 || b2 -> b1 \/ b2.
Proof. hammer_hook "HahnBase" "HahnBase.hahn__orb_split". intros [] []; auto. Qed.

Lemma hahn__norb_split : forall b1 b2, b1 || b2 = false -> b1 = false /\ b2 = false.
Proof. hammer_hook "HahnBase" "HahnBase.hahn__norb_split". intros [] []; auto. Qed.

Lemma hahn__eqb_split : forall b1 b2 : bool, (b1 -> b2) -> (b2 -> b1) -> b1 = b2.
Proof. hammer_hook "HahnBase" "HahnBase.hahn__eqb_split". intros [] [] H H'; unfold is_true in *; auto using sym_eq. Qed.

Lemma hahn__beq_rewrite : forall (T : eqType) (x1 x2 : T), eq_op x1 x2 -> x1 = x2.
Proof. hammer_hook "HahnBase" "HahnBase.hahn__beq_rewrite". by intros until 0; case eqP. Qed.

Hint Resolve hahn__internal_eqP neqP : hahn_refl.

Ltac hahn__complaining_inj f H :=
let X := fresh in
(match goal with | [|- ?P ] => set (X := P) end);
injection H; clear H; intros; subst X;
try subst.

Ltac hahn__clarify1 :=
try subst;
repeat match goal with
| [H: is_true (andb _ _) |- _] =>
let H' := fresh H in case (hahn__andb_split H); clear H; intros H' H
| [H: is_true (negb ?x) |- _] => rewrite (hahn__negb_rewrite H) in *
| [H: is_true ?x        |- _] => rewrite H in *
| [H: ?x = true         |- _] => rewrite H in *
| [H: ?x = false        |- _] => rewrite H in *
| [H: is_true (eq_op _ _)  |- _] => generalize (hahn__beq_rewrite H); clear H; intro H
| [H: @existT _ _ _ _ = @existT _ _ _ _ |- _] => apply inj_pair2 in H; try subst
| [H: ?f _             = ?f _             |- _] => hahn__complaining_inj f H
| [H: ?f _ _           = ?f _ _           |- _] => hahn__complaining_inj f H
| [H: ?f _ _ _         = ?f _ _ _         |- _] => hahn__complaining_inj f H
| [H: ?f _ _ _ _       = ?f _ _ _ _       |- _] => hahn__complaining_inj f H
| [H: ?f _ _ _ _ _     = ?f _ _ _ _ _     |- _] => hahn__complaining_inj f H
| [H: ?f _ _ _ _ _ _   = ?f _ _ _ _ _ _   |- _] => hahn__complaining_inj f H
| [H: ?f _ _ _ _ _ _ _ = ?f _ _ _ _ _ _ _ |- _] => hahn__complaining_inj f H
end; try done.

Ltac clarify :=
hahn__clarify1;
repeat match goal with
| H1: ?x = Some _, H2: ?x = None   |- _ => rewrite H2 in H1; discriminate
| H1: ?x = Some _, H2: ?x = Some _ |- _ => rewrite H2 in H1; hahn__clarify1
end;  try done.

Ltac vauto :=
(clarify; try edone;
try [> econstructor; (solve [edone | [> econstructor; edone]])]).

Ltac inv x := inversion x; clarify.
Ltac simpls  := simpl in *; try done.
Ltac ins := simpl in *; try done; intros.

Ltac hahn__clarsimp1 :=
clarify; (autorewrite with hahn_trivial hahn in * );
(autorewrite with hahn_trivial in * ); try done;
clarify; auto 1 with hahn.

Ltac clarsimp := intros; simpl in *; hahn__clarsimp1.

Ltac autos   := clarsimp; auto with hahn.

Tactic Notation "econs" := econstructor.
Tactic Notation "econs" int_or_var(x) := econstructor x.

Definition  NW (P: unit -> Prop) : Prop := P tt.

Notation "⟪ x : t ⟫" := (NW (fun x => t)) (at level 80, x ident, no associativity).
Notation "<< x : t >>" := (NW (fun x => t))
(at level 80, x ident, no associativity, only parsing).
Notation "⟪ t ⟫" := (NW (fun _ => t)) (at level 79, no associativity, format "⟪ t ⟫").

Ltac unnw := unfold NW in *.
Ltac rednw := red; unnw.

Hint Unfold NW.

Ltac splits :=
intros; unfold NW;
repeat match goal with
| [ |- _ /\ _ ] => split
end.

Ltac esplits :=
intros; unfold NW;
repeat match goal with
| [ |- @ex _ _ ] => eexists
| [ |- _ /\ _ ] => split
| [ |- @sig _ _ ] => eexists
| [ |- @sigT _ _ ] => eexists
| [ |- @prod _  _ ] => split
end.

Ltac desc :=
repeat match goal with
| H: is_true (eq_op _ _) |- _ => generalize (hahn__beq_rewrite H); clear H; intro H
| H : exists x, NW (fun y => _) |- _ =>
let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
| H : exists x, ?p |- _ =>
let x' := fresh x in destruct H as [x' H]
| H : ?p /\ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => red in x' | _ => idtac end;
match q with | NW _ => red in y' | _ => idtac end
| H : is_true (_ && _) |- _ =>
let H' := fresh H in case (hahn__andb_split H); clear H; intros H H'
| H : (_ || _) = false |- _ =>
let H' := fresh H in case (hahn__norb_split H); clear H; intros H H'
| H : ?x = ?x   |- _ => clear H

end.

Ltac des :=
repeat match goal with
| H: is_true (eq_op _ _) |- _ => generalize (hahn__beq_rewrite H); clear H; intro H
| H : exists x, NW (fun y => _) |- _ =>
let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
| H : exists x, ?p |- _ =>
let x' := fresh x in destruct H as [x' H]
| H : ?p /\ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => red in x' | _ => idtac end;
match q with | NW _ => red in y' | _ => idtac end
| H : is_true (_ && _) |- _ =>
let H' := fresh H in case (hahn__andb_split H); clear H; intros H H'
| H : (_ || _) = false |- _ =>
let H' := fresh H in case (hahn__norb_split H); clear H; intros H H'
| H : ?x = ?x |- _ => clear H
| H : ?p <-> ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => unfold NW at 1 in x'; red in y' | _ => idtac end;
match q with | NW _ => unfold NW at 1 in y'; red in x' | _ => idtac end
| H : ?p \/ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => H end in
destruct H as [x' | y'];
[ match p with | NW _ => red in x' | _ => idtac end
| match q with | NW _ => red in y' | _ => idtac end]
| H : is_true (_ || _) |- _ => case (hahn__orb_split H); clear H; intro H
| H : (_ && _) = false |- _ => case (hahn__nandb_split H); clear H; intro H
end.

Ltac cdes H :=
let H' := fresh H in assert (H' := H); red in H'; desc.

Ltac des_if_asm :=
clarify;
repeat
match goal with
| H: context[ match ?x with _ => _ end ] |- _ =>
match (type of x) with
| { _ } + { _ } => destruct x; clarify
| bool =>
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with hahn_refl);
subst P; destruct Heq as [Heq|Heq]
| _ => let Heq := fresh "Heq" in destruct x as [] eqn: Heq; clarify
end
end.

Ltac des_if_goal :=
clarify;
repeat
match goal with
| |- context[match ?x with _ => _ end] =>
match (type of x) with
| { _ } + { _ } => destruct x; clarify
| bool =>
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with hahn_refl);
subst P; destruct Heq as [Heq|Heq]
| _ => let Heq := fresh "Heq" in destruct x as [] eqn: Heq; clarify
end
end.

Ltac des_if :=
clarify;
repeat
match goal with
| |- context[match ?x with _ => _ end] =>
match (type of x) with
| { _ } + { _ } => destruct x; clarify
| bool =>
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with hahn_refl);
subst P; destruct Heq as [Heq|Heq]
| _ => let Heq := fresh "Heq" in destruct x as [] eqn: Heq; clarify
end
| H: context[ match ?x with _ => _ end ] |- _ =>
match (type of x) with
| { _ } + { _ } => destruct x; clarify
| bool =>
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with hahn_refl);
subst P; destruct Heq as [Heq|Heq]
| _ => let Heq := fresh "Heq" in destruct x as [] eqn: Heq; clarify
end
end.

Ltac des_eqrefl :=
match goal with
| H: context[match ?X with _ => _ end Logic.eq_refl] |- _ =>
let EQ := fresh "EQ" in
let id' := fresh "x" in
revert H;
generalize (Logic.eq_refl X); generalize X at 1 3;
intros id' EQ; destruct id'; intros H
| |- context[match ?X with _ => _ end Logic.eq_refl] =>
let EQ := fresh "EQ" in
let id' := fresh "x" in
generalize (Logic.eq_refl X); generalize X at 1 3;
intros id' EQ; destruct id'
end.

Ltac desf_asm := clarify; des; des_if_asm.

Ltac desf := clarify; des; des_if.

Ltac clarassoc := clarsimp; autorewrite with hahn_trivial hahn hahnA in *; try done.

Ltac hahn__hacksimp1 :=
clarsimp;
match goal with
| H: _ |- _ => solve [rewrite H; clear H; clarsimp
|rewrite <- H; clear H; clarsimp]
| _ => solve [f_equal; clarsimp]
end.

Ltac hacksimp :=
clarsimp;
try match goal with
| H: _ |- _ => solve [rewrite H; clear H; clarsimp
|rewrite <- H; clear H; clarsimp]
| |- context[match ?p with _ => _ end] => solve [destruct p; hahn__hacksimp1]
| _ => solve [f_equal; clarsimp]
end.

Ltac clarify_not :=
repeat (match goal with
| H : ~ False |- _ => clear H
| H : ~ ~ _ |- _ => apply NNPP in H
| H : ~ _ |- _ => apply imply_to_and in H; desc
| H : ~ _ |- _ => apply not_or_and in H; desc
| H : ~ _ |- _ => apply not_and_or in H; des
| H : ~ _ |- _ => apply not_all_ex_not in H; desc
end; clarify).

Tactic Notation "tertium_non_datur" constr(P) :=
destruct (classic P); clarify_not.

Tactic Notation "tertium_non_datur" constr(P) "as" simple_intropattern(pattern) :=
destruct (classic P) as pattern; clarify_not.

Tactic Notation "pattern_lhs" uconstr(term) :=
match goal with
|- _ ?lhs _ =>
let P := fresh in
pose (P := lhs); pattern term in P; change lhs with P; subst P
end.

Tactic Notation "pattern_rhs" uconstr(term) :=
match goal with
|- _ _ ?rhs =>
let P := fresh in
pose (P := rhs); pattern term in P; change rhs with P; subst P
end.

Tactic Notation "forward" tactic1(tac) :=
let foo := fresh in
evar (foo : Prop); cut (foo); subst foo; cycle 1; [tac|].

Tactic Notation "forward" tactic1(tac) "as" simple_intropattern(H) :=
let foo := fresh in
evar (foo : Prop); cut (foo); subst foo; cycle 1; [tac|intros H].

Tactic Notation "specialize_full" ident(H) :=
let foo := fresh in
evar (foo : Prop); cut (foo); subst foo; cycle 1; [eapply H|try clear H; intro H].

Ltac exploit x :=
refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _) _)
|| refine ((fun x y => y x) (x _ _) _)
|| refine ((fun x y => y x) (x _) _).

author: lukaszcz

repo: coqhammer-eval


text:
Require Export Pig.Relations.

Definition can_join_by (s: schema_ty) (c: col): Prop :=
  schema_column_has_type s c CTyNat.

Fixpoint schema_concatenation (s1 s2 : schema_ty): schema_ty :=
  match s1 with
  | STyNil => s2
  | c *** => STyPair c s2
  | c *** s1' => c *** (schema_concatenation s1' s2)
  end.

Notation "x +++ y" := (schema_concatenation x y) (at level 51, right associativity).

Inductive concatenated_schema: schema_ty -> schema_ty -> schema_ty -> Prop :=
| CatSchemaZeroAttr: forall s,
    concatenated_schema STyNil s s
| CatSchemaOneAttr: forall a s,
    concatenated_schema (a ***) s (a *** s)
| CatSchemaCons: forall a s1 s2 s3,
    concatenated_schema s1 s2 s3 ->
    concatenated_schema (a *** s1) s2 (a *** s3).

Lemma schema_concatenation_correct: forall (s1 s2: schema_ty),
  concatenated_schema s1 s2 (schema_concatenation s1 s2).
Proof.
  intros. induction s1.
  - admit.
  - admit.
Admitted.

(* IDEA: Maybe we don't need to model the tuples themselves, just their types.
         However, we do need to represent sorted lists of tuples, but we can
         do that using types (see stdlib's `Sorted`). Because of this I am
         hoping that we don't need to `fuse_tuples`. *)

(*
Fixpoint fuse_tuples (s1 s2: schema_ty) (t1: support s1) (t2: support s2) :
                                     support (schema_concatenation s1 s2) := ???
*)

Inductive joined (s1 s2: schema_ty): relation s1 -> col ->
                                     relation s2 -> col ->
                                     relation (s1 +++ s2) -> Prop :=
  | Joined : forall (r1: relation s1) (r2: relation s2) (c1 c2: col)
                    (r': relation (s1 +++ s2)),
     (* TODO: Add constraints. *)
     joined s1 s2 r1 c1 r2 c2 r'.

repo: axum