text:
Require Import HoareDef IntroHeader IntroF0 IntroF1 SimModSem.
Require Import Coqlib.
Require Import ImpPrelude.
Require Import Skeleton.
Require Import PCM.
Require Import ModSem Behavior.
Require Import Relation_Definitions.

(*** TODO: export these in Coqlib or Universe ***)
Require Import Relation_Operators.
Require Import RelationPairs.
From ITree Require Import
     Events.MapDefault.
From ExtLib Require Import
     Core.RelDec
     Structures.Maps
     Data.Map.FMapAList.

Require Import HTactics.

Set Implicit Arguments.

Local Open Scope nat_scope.

Section SIMMODSEM.

  Context `{Σ: GRA.t}.

  Let W: Type := Any.t * Any.t.

  Let wf: unit -> W -> Prop :=
    fun _ '(mrps_src0, mrps_tgt0) =>
      (<<SRC: mrps_src0 = tt↑>>) /\
      (<<TGT: mrps_tgt0 = tt↑>>)
  .

  Theorem correct:
    refines2 [IntroF0.F] [IntroF1.F].
  Proof.
    eapply adequacy_local2. econs; ss. i.
    econstructor 1 with (wf:=wf) (le:=top2); et; ss.
    econs; ss. init. unfold cfunU.
    unfold fF, IntroF0.fF.
    steps. des. clarify. ss. steps.
    force_r. { eapply max_intrange; ss. } steps.
    destruct (Z.of_nat x <? 0)%Z eqn:T; try lia.
    unfold Ncall.
    destruct (Z.of_nat x =? 0)%Z eqn:U.
    { steps. assert(x = 0) by lia. steps. force_l. exists false. steps. force_l. eexists (Vint 0). steps.
      force_l; ss. steps. force_l. eexists (Vint _). steps. force_l; ss. steps. r. esplits; et.
    }
    steps. destruct x0.
    - force_l. exists true. unfold ccallU. steps.
      rewrite Z.eqb_neq in *. force_l; ss. { splits; try lia. eapply OrdArith.lt_from_nat. lia. } steps.
      force_r. { f_equal. lia. } steps.
      force_l. eexists. steps. force_l; ss. steps. r. esplits; et. do 2 f_equal. lia.
    - steps. force_l. exists false. steps. force_l. eexists. steps. force_l; ss. steps.
      force_l. esplits. steps. force_l; ss. steps. r. esplits; et. do 2 f_equal. lia.
  Unshelve. all: try exact 0. all: ss.
  Qed.

End SIMMODSEM.

author: alxest

repo: CCR

save_path: github-repos/coq/alxest-CCR


text:
Require Import sflib.

Require Import Axioms.
Require Import Basic.
Require Import DataStructure.
Require Import Loc.
Require Import Language.

Require Import Time.
Require Import Event.
Require Import View.
Require Import Cell.
Require Import Memory.
Require Import TView.
Require Import Local.
Require Import Thread.

Set Implicit Arguments.

(** * The Program Step in the Promising Semantics 2.1 *)

(** This file defines the program steps (machine steps) in promising semantics 2.1. *)
(** The program steps in PS2.1 defined in this file corresponds to
    the definitions in Figure 9 in our paper. *)

Module Threads.

  (** ** Thread Pool  *)
  (** It is a set of threads and corresponds to (ThrdPool) in paper. *)
  Definition t := IdentMap.t ({lang:language & (Language.state lang)} * Local.t).

  (** Add new threads in the thread pool (for initialization). *)
  Definition add_th {lang: language}
             (ths:t) (tid:IdentMap.key) (f: Language.fid) (code: Language.syntax lang) : option t :=
    match ((Language.init lang) code f) with
    | Some s => Some (IdentMap.add tid (existT _ _ s, Local.init) ths)
    | _ => None
    end.

  Definition tid_incr := POrderedType.Positive_as_DT.succ.
  Fixpoint add_ths {lang: language}
           (ths: t) (tid: IdentMap.key) (fs: list Language.fid) (code: Language.syntax lang) : option t :=
    match fs with
    | f::fs' => match add_ths ths (tid_incr tid) fs' code with
               | Some ths' => add_th ths' tid f code
               | _ => None
               end
    | _ => Some ths
    end.

  Definition empty_ths := IdentMap.empty ({lang:language & (Language.state lang)} * Local.t).

  Definition init {lang: language} (fs: list Language.fid) (code: Language.syntax lang) :=
    add_ths empty_ths BinNums.xH fs code.

  Definition is_terminal (ths:t): Prop :=
    forall tid lang st lc (FIND: IdentMap.find tid ths = Some (existT _ lang st, lc)),
      <<STATE: (Language.is_terminal lang) st>> /\
      <<THREAD: Local.is_terminal lc>>.

  Inductive wf (ths:t) (mem:Memory.t): Prop :=
  | wf_intro
      (DISJOINT:
         forall tid1 lang1 st1 lc1
           tid2 lang2 st2 lc2
           (TID: tid1 <> tid2)
           (TH1: IdentMap.find tid1 ths = Some (existT _ lang1 st1, lc1))
           (TH2: IdentMap.find tid2 ths = Some (existT _ lang2 st2, lc2)),
           Local.disjoint lc1 lc2)
      (THREADS: forall tid lang st lc
                  (TH: IdentMap.find tid ths = Some (existT _ lang st, lc)),
          Local.wf lc mem)
  .

  Definition consistent (ths:t) (sc:TimeMap.t) (mem:Memory.t) (lo: Ordering.LocOrdMap): Prop :=
    forall tid lang st lc
      (TH: IdentMap.find tid ths = Some (existT _ lang st, lc)),
      Thread.consistent (Thread.mk lang st lc sc mem) lo.

  Definition consistent_nprm (ths:t) (sc:TimeMap.t) (mem:Memory.t) (lo: Ordering.LocOrdMap): Prop :=
    forall tid lang st lc
      (TH: IdentMap.find tid ths = Some (existT _ lang st, lc)),
      Thread.consistent_nprm (Thread.mk lang st lc sc mem) lo.

  Inductive is_promised tid (loc:Loc.t) (to:Time.t) (threads:t): Prop :=
  | is_promised_intro
      lang st lc from msg
      (TID: IdentMap.find tid threads = Some (existT _ lang st, lc))
      (PROMISES: Memory.get loc to (Local.promises lc) = Some (from, msg))
  .

  (* tids *)

  Definition tids (ths: t): IdentSet.t :=
    List.fold_right (fun p s => IdentSet.add (fst p) s) IdentSet.empty (IdentMap.elements ths).
End Threads.

Module Configuration.
  (** ** Program Configuration *)
  (** The program configuration in promising semantics 2.1. It includes:
      - [threads]: thread pool;
      - [tid]: the identifier of the current thread;
      - [sc]: the timemap for SC fence;
      - [memory]: memory shared by all threads;

      It corresponds to (World) in paper. *)
  Structure t := mk {
    threads: Threads.t;
    tid: IdentMap.key;
    sc: TimeMap.t;
    memory: Memory.t;
  }.

  (** ** Initialization of the Program in the Promising Semantics 2.1 *)
  Definition init {lang: language} (fs: list Language.fid) (code: Language.syntax lang) (ctid: IdentMap.key) :=
    match (Threads.init fs code) with
    | Some ths => Some (mk ths ctid TimeMap.bot Memory.init)
    | _ => None
    end.

  Definition is_terminal (conf:t): Prop := Threads.is_terminal (threads conf).

  Inductive wf (conf:t): Prop :=
  | wf_intro
      (WF: Threads.wf (threads conf) (memory conf))
      (SC: Memory.closed_timemap (sc conf) (memory conf))
      (MEM: Memory.closed (memory conf))
  .

  Definition sw_tid (c1: t) (new_tid: IdentMap.key): t := mk (threads c1) new_tid (sc c1) (memory c1).
  Lemma tid_eq_dec: forall (tid1 tid2: IdentMap.key),
      {tid1 = tid2} + {tid1 <> tid2}.
  Proof. eapply IdentSet.Raw.L.MO.eq_dec; eauto. Qed.

  Lemma sw_to_self
        c:
    c = sw_tid c (tid c).
  Proof.
    destruct c; ss.
  Qed.

  Lemma sw_tid_twice
        c tid1 tid2:
    Configuration.sw_tid (Configuration.sw_tid c tid1) tid2 =
    Configuration.sw_tid c tid2.
  Proof.
    destruct c; ss.
  Qed.

  Definition consistent (lo: Ordering.LocOrdMap) (c: t): Prop :=
    Threads.consistent (threads c) (sc c) (memory c) lo.

  Definition no_promise (c: t): Prop :=
    forall tid lang st lc (FIND: IdentMap.find tid (threads c) = Some (existT _ lang st, lc)),
      (Local.promises lc) = Memory.bot.

  (** ** Program Step *)
  (** Program step (or machine step) in promising semantics 2.1.
      It takes four parameters:
      - [e]: machine event;
      - [lo]: a set of atomic locations;
      - [c1] and [c2]: program configurations before and after transition. *)
  Inductive step: forall (e:MachineEvent.t) (lo: Ordering.LocOrdMap) (c1 c2:t), Prop :=
  | step_tau
      lang lo c1 c2 st1 st2 lc1 lc2 e1 tid1
      (CTID: tid c1 = tid1)
      (TID1: IdentMap.find tid1 (threads c1) = Some (existT _ lang st1, lc1))
      (STEPS: rtc (@Thread.tau_step _ lo) (Thread.mk _ st1 lc1 (sc c1) (memory c1)) e1)
      (STEP: Thread.tau_step lo e1 (Thread.mk _ st2 lc2 (sc c2) (memory c2)))
      (** The execution of current thread must reach a promise certified state. *)
      (CONSISTENT: Thread.consistent (Thread.mk _ st2 lc2 (sc c2) (memory c2)) lo)
      (C2: c2 = mk (IdentMap.add tid1 (existT _ _ st2, lc2) (threads c1)) tid1 (sc c2) (memory c2)):
      step MachineEvent.silent lo c1 c2
  | step_out
      lang lo c1 c2 st1 st2 lc1 lc2 e1 e tid1
      (CTID: tid c1 = tid1)
      (TID1: IdentMap.find tid1 (threads c1) = Some (existT _ lang st1, lc1))
      (STEPS: rtc (@Thread.tau_step _ lo) (Thread.mk _ st1 lc1 (sc c1) (memory c1)) e1)
      (STEP_OUT: Thread.out_step lo e e1 (Thread.mk _ st2 lc2 (sc c2) (memory c2)))
      (CONSISTENT: Thread.consistent (Thread.mk _ st2 lc2 (sc c2) (memory c2)) lo)
      (C2: c2 = mk (IdentMap.add tid1 (existT _ _ st2, lc2) (threads c1)) tid1 (sc c2) (memory c2)):
      step (MachineEvent.syscall e) lo c1 c2
  | step_sw
      tid' lang c1 c2 st2 lc2 lo
      (TID2_OK: IdentMap.find tid' (threads c1) = Some (existT _ lang st2, lc2))
      (C2: c2 = Configuration.mk (threads c1) tid' (sc c1) (memory c1)):
      step MachineEvent.switch lo c1 c2
  | step_thread_term
      lang c1 c2 st1 lc1 st2 lc2 lo tid1 tid'
      (CTID: tid c1 = tid1)
      (OLD_TID: IdentMap.find tid1 (threads c1) = Some (existT _ lang st1, lc1))
      (THRD_DONE: Thread.is_done (Thread.mk _ st1 lc1 (sc c1) (memory c1)))
      (THRDS_REMOVE: ((IdentMap.remove tid1 (threads c1)) = (threads c2)))
      (NEW_TID_OK: IdentMap.find tid' (threads c2) = Some (existT _ lang st2, lc2))
      (C2: c2 = mk (threads c2) tid' (sc c1) (memory c1)):
      step MachineEvent.switch lo c1 c2
  .
  Hint Constructors step.

  (** ** Done Configuration *)
  (** All of threads terminate. *)
  Definition is_done (c: t): Prop :=
    exists lang st lc,
      (IdentMap.find (tid c) (threads c) = Some (existT _ lang st, lc)) /\
      Thread.is_done (Thread.mk _ st lc (sc c) (memory c)) /\
      IdentMap.is_empty (IdentMap.remove (tid c) (threads c)) = true.

  Definition is_abort (c: t) (lo: Ordering.LocOrdMap): Prop :=
      exists lang st1 lc1  e',
        IdentMap.find (tid c) (threads c) = Some (existT _ lang st1, lc1) /\
        rtc (@Thread.tau_step _ lo) (Thread.mk _ st1 lc1 (sc c) (memory c)) e' /\
        Thread.is_abort e' lo.

  Inductive tau_step: Ordering.LocOrdMap -> t -> t -> Prop :=
  | tau_step_intro
      e lo c1 c2
      (WP_STEP: step e lo c1 c2)
      (TAU: ~(exists e0, e = MachineEvent.syscall e0)):
      tau_step lo c1 c2.

  Inductive all_step: Ordering.LocOrdMap -> t -> t -> Prop :=
  | all_step_intro
      e lo c1 c2
      (WP_STEP: step e lo c1 c2):
      all_step lo c1 c2.

  (** ** Abort Configuration *)
  Inductive abort_config: forall (lo: Ordering.LocOrdMap) (c: t), Prop :=
  | Abort_config_intro
      lo c c'
      (STEPS: rtc (all_step lo) c c')
      (ABORT: is_abort c' lo):
      abort_config lo c.

  (** ** Safe Program *)
  (** A program is safe, if its executions will never reach an abort configuration. *)
  Inductive safe {lang: language} :
    forall (lo: Ordering.LocOrdMap) (fs: list Language.fid) (code: Language.syntax lang) (ctid: IdentMap.key), Prop :=
  | Safe_intro
      lo fs code ctid
      (SAFR_EXEC: forall c, init fs code ctid = Some c -> ~(abort_config lo c)):
      safe lo fs code ctid.

  (** Aux promising semantics (machine step).
    1. same init/term/sw/done/abort rule, done/abort definition
    2. we have na/prc/atm step now (substitute for single tau step)
    *)
  Inductive aux_step: forall (e:AuxEvent.t) (lo: Ordering.LocOrdMap) (c1 c2:t), Prop :=
  | aux_step_na
    lang lo c1 c2 st1 st2 lc1 lc2 e1 tid1
    (CTID: tid c1 = tid1)
    (TID1: IdentMap.find tid1 (threads c1) = Some (existT _ lang st1, lc1))
    (STEPS: rtc (@Thread.na_step _ lo) (Thread.mk _ st1 lc1 (sc c1) (memory c1)) e1)
    (STEP: Thread.na_step lo e1 (Thread.mk _ st2 lc2 (sc c2) (memory c2)))
    (CONSISTENT: Thread.consistent (Thread.mk _ st2 lc2 (sc c2) (memory c2)) lo)
    (C2: c2 = mk (IdentMap.add tid1 (existT _ _ st2, lc2) (threads c1)) tid1 (sc c2) (memory c2)):
    aux_step AuxEvent.na lo c1 c2
  | aux_step_prc
    lang lo c1 c2 st1 st2 lc1 lc2 e1 tid1
    (CTID: tid c1 = tid1)
    (TID1: IdentMap.find tid1 (threads c1) = Some (existT _ lang st1, lc1))
    (STEPS: rtc (@Thread.prc_step _ lo) (Thread.mk _ st1 lc1 (sc c1) (memory c1)) e1)
    (STEP: Thread.prc_step lo e1 (Thread.mk _ st2 lc2 (sc c2) (memory c2)))
    (CONSISTENT: Thread.consistent (Thread.mk _ st2 lc2 (sc c2) (memory c2)) lo)
    (C2: c2 = mk (IdentMap.add tid1 (existT _ _ st2, lc2) (threads c1)) tid1 (sc c2) (memory c2)):
    aux_step AuxEvent.prc lo c1 c2
  | aux_step_at
    lang lo c1 c2 st1 st2 lc1 lc2 e1 e1' tid1
    (CTID: tid c1 = tid1)
    (TID1: IdentMap.find tid1 (threads c1) = Some (existT _ lang st1, lc1))
    (STEPS_PRC: rtc (@Thread.prc_step _ lo) (Thread.mk _ st1 lc1 (sc c1) (memory c1)) e1)
    (STEPS_ATM: rtc (@Thread.atmblk_step _ lo) e1 e1')
    (STEP_ATM: Thread.atmblk_step lo e1' (Thread.mk _ st2 lc2 (sc c2) (memory c2)))
    (CONSISTENT: Thread.consistent (Thread.mk _ st2 lc2 (sc c2) (memory c2)) lo)
    (C2: c2 = mk (IdentMap.add tid1 (existT _ _ st2, lc2) (threads c1)) tid1 (sc c2) (memory c2)):
    aux_step AuxEvent.atm lo c1 c2
  | aux_step_out
    lang lo c1 c2 st1 st2 lc1 lc2 e1 e tid1
    (CTID: tid c1 = tid1)
    (TID1: IdentMap.find tid1 (threads c1) = Some (existT _ lang st1, lc1))
    (STEPS: rtc (@Thread.na_step _ lo) (Thread.mk _ st1 lc1 (sc c1) (memory c1)) e1)
    (STEP_OUT: Thread.out_step lo e e1 (Thread.mk _ st2 lc2 (sc c2) (memory c2)))
    (CONSISTENT: Thread.consistent (Thread.mk _ st2 lc2 (sc c2) (memory c2)) lo)
    (C2: c2 = mk (IdentMap.add tid1 (existT _ _ st2, lc2) (threads c1)) tid1 (sc c2) (memory c2)):
    aux_step (AuxEvent.out e) lo c1 c2
  | aux_step_sw
      tid' lang c1 c2 st2 lc2 lo
      (TID2_OK: IdentMap.find tid' (threads c1) = Some (existT _ lang st2, lc2))
      (C2: c2 = Configuration.mk (threads c1) tid' (sc c1) (memory c1)):
      aux_step AuxEvent.sw lo c1 c2
  | aux_step_thread_term
      lang c1 c2 st1 lc1 st2 lc2 lo tid1 tid'
      (CTID: tid c1 = tid1)
      (OLD_TID: IdentMap.find tid1 (threads c1) = Some (existT _ lang st1, lc1))
      (THRD_DONE: Thread.is_done (Thread.mk _ st1 lc1 (sc c1) (memory c1)))
      (THRDS_REMOVE: ((IdentMap.remove tid1 (threads c1)) = (threads c2)))
      (NEW_TID_OK: IdentMap.find tid' (threads c2) = Some (existT _ lang st2, lc2))
      (C2: c2 = mk (threads c2) tid' (sc c1) (memory c1)):
      aux_step AuxEvent.tterm lo c1 c2
  .
  Hint Constructors aux_step.

  Inductive aux_tau_step: Ordering.LocOrdMap -> t -> t -> Prop :=
  | aux_tau_step_intro
      e lo c1 c2
      (WP_STEP: aux_step e lo c1 c2)
      (TAU: ~(exists e0, e = AuxEvent.out e0)):
    aux_tau_step lo c1 c2.

  Inductive aux_all_step: Ordering.LocOrdMap -> t -> t -> Prop :=
  | aux_all_step_intro
      e lo c1 c2
      (WP_STEP: aux_step e lo c1 c2):
    aux_all_step lo c1 c2.

End Configuration.

author: Hughshine

repo: promising-comp


text:
Require Import Auxiliaries.
Require Import Nat List Bool Arith Omega.

From QuickChick Require Import QuickChick.
Import ListNotations.
Import QcDefaultNotation. Open Scope qc_scope.
Import GenLow GenHigh.

Require Import Coq.Structures.Equalities.

(**
  Just to be sure, the correctness of some of our definitions and lemmas are
  "proved" with QuickChick
*)

Module NatType <: Typ with Definition t := nat.
Definition t := nat.
End NatType.

Module InserterRemoverOverNat := (NthInserterRemover NatType).
Import InserterRemoverOverNat.

Definition genInput : G (nat * (list nat)) :=
  genPair (choose (0, 100)) (listOf (choose (0, 100))).

Definition nth_remove_length_check n (l : list nat) :=
  ((n <? length l) && ((length (nth_remove n l)) =? (pred (length l))))
  ||
  ((length l <=? n) && ((length (nth_remove n l)) =? (length l))).

Definition nth_insert_length_check n (l: list nat) x :=
  ((n <=? length l) && (length (nth_insert n l x) =? (succ (length l))))
  ||
  ((length l <? n) && ((length (nth_insert n l x)) =? (length l))).

Definition nth_insert_prop n (l : list nat) x :=
  ((n <=? length l) &&
   (0 <? length (filter (fun x' => (x' =? x)) (nth_insert n l x))))
  || (length l <? n).

Definition qc_test_remove_length (nl: prod nat (list nat)) :=
  nth_remove_length_check (fst nl) (snd nl).
Definition qc_test_insert_length (nl: prod nat (list nat)) :=
  nth_insert_length_check (fst nl) (snd nl).
Definition qc_test_insert_prop (nl: prod nat (list nat)) :=
  nth_insert_prop (fst nl) (snd nl).

QuickChick (forAll genInput qc_test_remove_length).
QuickChick (forAll genInput qc_test_insert_length).
QuickChick (forAll genInput qc_test_insert_prop).

author: holmuk

repo: coq-zipper

save_path: github-repos/coq/holmuk-coq-zipper


text:
From Coq Require Import Extraction.
From Coq Require Import List.
Declare ML Module "coq_spec".
From Hammer Require Import Hammer.
From Hammer Require Import Reconstr.
Add LoadPath "~/Documents/cpdt/src" as Cpdt.
Require Import Cpdt.CpdtTactics.
Open Scope list_scope.

MaxTermSize 5.
MaxTestSize 20.

From Coq Require Import ZArith.BinIntDef.
Module ZZ := BinIntDef.Z.
Print ZZ.

Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
Extract Inductive unit => "()" [ "()" ].
Extract Inductive list => "([])" [ "([])" "(:)" ].
Extract Inductive prod => "(,)" [ "(,)" ].

Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
Extract Inductive sumor => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].

Extract Inlined Constant andb => "(Prelude.&&)".
Extract Inlined Constant orb => "(Prelude.||)".
Extract Inlined Constant negb => "Prelude.not".

(* not needed to prove the laws of groups, but can be useful for clarity *)
Definition isUnit (n : Z) := ZZ.eqb n ZZ.zero.

Definition zadd := ZZ.add.

(* DiscoverLemmas "ZGroupTest" zadd isUnit. *)

(* result with zadd:
== Laws ==
  1. zadd x y = zadd y x
  2. zadd x Z0 = x
  3. zadd (zadd x y) z = zadd x (zadd y z)
  4. zadd (Zneg x) (Zneg x) = Zneg (XO x)
  5. zadd (Zneg x) (Zpos x) = Z0
  6. zadd (Zpos x) (Zpos x) = Zpos (XO x)

  3. is associativity law for group
  2. and 1. implies identity element law for group
  5. and 1. implies inverse element law for group
  Note: the Closure law doesn't make sense here because it is internalized in the underlying type theory.
 *)

(* results with isUnit included:
  1. isUnit x & isUnit y => x = y
  2. isUnit x => Z0 = x
  3. zadd x y = zadd y x
  4. isUnit y => zadd x y = x
  5. isUnit (Zneg x) = False
  6. isUnit (Zpos x) = False
  7. isUnit (zadd x x) = isUnit x
  8. zadd (zadd x y) z = zadd x (zadd y z)
  9. zadd (Zneg x) (Zneg x) = Zneg (XO x)
 10. isUnit y => zadd (Zneg x) (Zpos x) = y
 11. zadd (Zpos x) (Zpos x) = Zpos (XO x)

  1. is the law of uniqueness of unit
  4. is another way of formulating the identity law.
  10. is another way of formulating the inverse element law.
*)

(*  Lemma lemma_1 :
  forall (x : Z) (y : Z),
  (zadd y x) = (zadd x y).
  Proof. crush. Qed.
Lemma lemma_2 :
  forall (x : Z),
  (zadd x Z0) = x.
  Proof. crush. Qed.
Lemma lemma_3 :
  forall (x : Z) (y : Z) (z : Z),
  (zadd (zadd x y) z) = (zadd x (zadd y z)).
  Proof. crush. Qed.
Lemma lemma_4 :
  forall (x : positive),
  (zadd (Zneg x) (Zneg x)) = (Zneg (xO x)).
  Proof. hammer. Qed.
Lemma lemma_5 :
  forall (x : positive),
  (zadd (Zneg x) (Zpos x)) = Z0.
  Proof. crush. hammer. Qed.
Lemma lemma_6 :
  forall (x : positive),
  (zadd (Zpos x) (Zpos x)) = (Zpos (xO x)).
  Proof. crush. hammer. Qed. *)

author: mikkelmilo

repo: rooster-spec


text:
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesCurried.

Local Open Scope cat.

Section local_helper_lemmas.
  (* I would assume that the following lemmas should already exists in the "iso file", but I can't find it (I need is_iso_stable_undertransportation)  *)
  Lemma iso_stable_under_equality {C : category} {x y : C} {f g : C⟦x,y⟧} : (g = f) → (is_z_isomorphism f) → (is_z_isomorphism g).
  Proof.
    intros pe pi.
    induction pe.
    exact pi.
  Qed.

  Lemma iso_stable_under_tranportation {C : category} {x y z : C} {f : C⟦x,y⟧} {pf : y=z} : (is_z_isomorphism f) → (is_z_isomorphism (transportf _ pf f)).
  Proof.
    intro pfi.
    induction pf.
    use pfi.
  Qed.

  Lemma iso_stable_under_equalitytransportation {C : category} {x y z : C} {f : C⟦x,y⟧} {g : C⟦x,z⟧} {pf : y=z} :
    (g = transportf _ pf f) -> (is_z_isomorphism f) -> (is_z_isomorphism g).
  Proof.
    intros p isof.
    use (iso_stable_under_equality p).
    use (iso_stable_under_tranportation).
    exact isof.
  Qed.
End local_helper_lemmas.

Section Curried_Monoidal_Functors.

  Context (C D : category) (M : monoidalcategory_data C) (N : monoidalcategory_data D) (F : functor C D).

  Notation "x ⊗_{ M } y" := ((tensoronobjects_from_tensordata M) x y) (at level 31).
  Notation "f ⊗^{ M } g" := ((tensoronmorphisms_from_tensordata M) _ _ _ _ f g) (at level 31).
  Notation "I_{ M }" := (unit_from_monoidalcatdata M).
  Notation "lu^{ M }_{ x }" := (leftunitordata_from_monoidalcatdata M x ).
  Notation "ru^{ M }_{ x }" := (rightunitordata_from_monoidalcatdata M x ).
  Notation "α^{ M }_{ x , y , z }" := ((associatordata_from_monoidalcatdata M) x y z).

  (** (Weak) Monoidal functors **)
  (* Monoidal functor data *)
  Definition tensor_preserving_data : UU
    := ∏ (x y : C), D⟦(F x) ⊗_{N} (F y), F (x ⊗_{M} y)⟧.

  Definition unit_preserving_data : UU := D ⟦ I_{N} , F I_{M} ⟧.

  Definition monoidalfunctor_data :=
    tensor_preserving_data × unit_preserving_data.

  Definition tensorpreservingdata_from_monoidalfunctordata (mfd : monoidalfunctor_data) : tensor_preserving_data := pr1 mfd.
  Coercion tensorpreservingdata_from_monoidalfunctordata : monoidalfunctor_data >-> tensor_preserving_data.

  Definition unitpreservingdata_from_monoidalfunctordata (mfd : monoidalfunctor_data) : unit_preserving_data := pr2 mfd.
  Coercion unitpreservingdata_from_monoidalfunctordata : monoidalfunctor_data >-> unit_preserving_data.

  (* Weak monoidal functor properties *)
  Definition tensor_preserving_data_is_natural (tpd : tensor_preserving_data) :=
    ∏ (x y x' y' : C) (f : C⟦x,x'⟧) (g : C⟦y,y'⟧),
      (#F (f ⊗^{M} g))∘(tpd x y) = (tpd x' y')∘((#F f) ⊗^{N} (#F g)).

  Definition preserves_associativity (tpd : tensor_preserving_data) :=
    ∏ (x y z : C), (#F (α^{M}_{x,y,z})) ∘ (tpd (x ⊗_{M} y) z) ∘ ((tpd x y) ⊗^{N} (identity (F z)))
                   = (tpd x (y ⊗_{M} z)) ∘ ((identity (F x)) ⊗^{N} (tpd y z)) ∘ α^{N}_{F x, F y, F z}.

  Definition preserves_leftunitality (tpd : tensor_preserving_data) (upd : unit_preserving_data) : UU :=
    ∏ (x : C), ((#F (lu^{M}_{x})) ∘ (tpd I_{M} x) ∘ (upd ⊗^{N} (identity (F x)))) = lu^{N}_{F x}.

  Definition preserves_rightunitality (tpd : tensor_preserving_data) (upd : unit_preserving_data) : UU :=
    ∏ (x : C), (#F (ru^{M}_{x})) ∘ (tpd x I_{M}) ∘ ((identity (F x)) ⊗^{N} upd) = ru^{N}_{F x}.

  Definition monoidalfunctor_laws (mfd : monoidalfunctor_data) : UU :=
    (tensor_preserving_data_is_natural mfd) × (preserves_associativity mfd) ×
    (preserves_leftunitality mfd mfd) × (preserves_rightunitality mfd mfd).

  Definition monoidalfunctor : UU :=
    ∑ (mfd : monoidalfunctor_data), monoidalfunctor_laws mfd.

  (** Strong and strict monoidal properties *)

  Definition is_stronglytensorpreserving (tpd : tensor_preserving_data) : UU :=
    ∏ (x y : C), is_z_isomorphism (tpd x y).

  Definition is_strictlytensorpreserving (tpd : tensor_preserving_data) : UU :=
      ∏ (x y : C), ∑ (pf : (F x) ⊗_{N} (F y) = F (x ⊗_{M} y)),
      (tpd x y ) = transportf _ pf (identity ((F x) ⊗_{N} (F y))).

  Lemma strictlytensorpreserving_is_strong {tpd : tensor_preserving_data} (pfstrict : is_strictlytensorpreserving tpd) : is_stronglytensorpreserving tpd.
  Proof.
    intros x y.
    use (iso_stable_under_equalitytransportation (pr2 (pfstrict x y)) (is_z_isomorphism_identity ((F x) ⊗_{N} (F y)))).
  Defined.
  Coercion strictlytensorpreserving_is_strong : is_strictlytensorpreserving >-> is_stronglytensorpreserving.

  Definition is_stronglyunitpreserving (upd : unit_preserving_data) : UU := is_z_isomorphism upd.

  Definition is_strictlyunitpreserving (upd : unit_preserving_data) : UU :=
    ∑ (pf : I_{N} = (F I_{M})), upd = transportf _ pf (identity I_{N}).

  Definition strictlyunitpreserving_is_strong {upd : unit_preserving_data} (pfstrict : is_strictlyunitpreserving upd) : is_stronglyunitpreserving upd.
  Proof.
    use (iso_stable_under_equalitytransportation (pr2 pfstrict) (is_z_isomorphism_identity I_{N})).
  Defined.
  Coercion strictlyunitpreserving_is_strong : is_strictlyunitpreserving >-> is_stronglyunitpreserving.

End Curried_Monoidal_Functors.

author: UniMath

repo: UniMath

save_path: github-repos/coq/UniMath-UniMath


text:
Definition Seq{A:Type} := nat -> A.

Definition sin{A : Type}(a : A)(q: Seq(A:=A)) := exists i, a = q i.

Lemma sin_nth{A:Type}(q: Seq(A:=A)): forall n,  sin (q n) q.
Proof.
intro n.
now exists n.
Qed.

Definition increasing {A: Type} (R: A -> A -> Prop)(q : Seq) : Prop  :=
  forall n,  R (q n) (q (S n)).

Definition strictly_increasing{A : Type}(R: A -> A -> Prop)(q : Seq(A := A)) :=
  increasing R q /\
forall n,  ~R (q (S n)) (q n).

Lemma increasing_snth{A : Type}
      (R : A -> A -> Prop)
      (RRefl : forall a,  R a a)
      (Rtrans : forall a b c,  R a b -> R b c -> R a c)
  : forall (q: Seq (A := A)),
    increasing R q  -> forall (i j : nat),  i <= j -> R (q i) (q j).
Proof.
intros q Hr i j Hle.
induction Hle.
*
  apply RRefl.
*
  specialize (Hr m).
  eapply Rtrans  ; eauto.
Qed.

Definition sup{A: Type} (R : A -> A-> Prop) (sup_val: A) (q : Seq(A:=A)) :=
  (forall a, sin a q -> R a sup_val) /\
  (forall sup_val',  (forall a, sin a q -> R a sup_val')  -> R sup_val sup_val').

author: hidden-author


text:
Load LFindLoad.
From lfind Require Import LFind.
From QuickChick Require Import QuickChick.
From adtind Require Import goal33.

Derive Show for natural.

              Derive Arbitrary for natural.

              Instance Dec_Eq_natural : Dec_Eq natural.

              Proof. dec_eq. Qed.

Lemma conj1synthconj6 : forall  (lv0 : natural) (lv1 : natural), (@eq natural (lv0) lv1).
Admitted.
QuickChick conj1synthconj6.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


(** * Linearize: Place all and only operations in let binders *)
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Wf.
Require Import Crypto.Compilers.ExprInversion.
Require Import Crypto.Compilers.WfInversion.
Require Import Crypto.Compilers.WfProofs.
Require Import Crypto.Compilers.Linearize.
Require Import Crypto.Util.Sigma.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.DestructHead.

Local Open Scope ctype_scope.
Section language.
  Context {base_type_code : Type}
          {op : flat_type base_type_code -> flat_type base_type_code -> Type}.

  Local Notation flat_type := (flat_type base_type_code).
  Local Notation type := (type base_type_code).
  Local Notation Tbase := (@Tbase base_type_code).
  Local Notation exprf := (@exprf base_type_code op).
  Local Notation expr := (@expr base_type_code op).
  Local Notation Expr := (@Expr base_type_code op).
  Local Notation wff := (@wff base_type_code op).
  Local Notation wf := (@wf base_type_code op).

  Section with_var.
    Context {var1 var2 : base_type_code -> Type}.

    Local Ltac t_fin_step tac :=
      match goal with
      | _ => assumption
      | _ => progress simpl in *
      | _ => progress subst
      | _ => progress inversion_sigma
      | _ => progress destruct_head'_sig
      | _ => progress destruct_head'_and
      | _ => setoid_rewrite List.in_app_iff
      | [ H : context[List.In _ (_ ++ _)] |- _ ] => setoid_rewrite List.in_app_iff in H
      | _ => progress intros
      | _ => solve [ eauto ]
      | _ => solve [ intuition (subst; eauto) ]
      | [ H : forall (x : prod _ _) (y : prod _ _), _ |- _ ] => specialize (fun x x' y y' => H (x, x') (y, y'))
      | _ => rewrite !List.app_assoc
      | [ H : _ \/ _ |- _ ] => destruct H
      | [ H : _ |- _ ] => apply H
      | [ H : forall G : list _, _ |- _ ] => apply (H nil)
      | _ => eapply wff_in_impl_Proper; [ solve [ eauto using wff_SmartVarf ] | solve [ repeat t_fin_step tac ] ]
      | _ => progress tac
      | [ |- wff _ _ _ ] => constructor
      | [ |- wf _ _ _ ] => constructor
      | _ => break_innermost_match_step
      | _ => progress inversion_expr
      | _ => congruence
      | _ => progress destruct_head' sum
      | _ => progress unfold invert_Op in *
      | _ => break_innermost_match_hyps_step
      end.
    Local Ltac t_fin tac := repeat t_fin_step tac.

    Local Hint Constructors Wf.wff.
    Local Hint Resolve List.in_app_or List.in_or_app.

    Section gen1.
      Context (let_bind_op_args : bool).

      Fixpoint wff_under_letsf' G {t} e1 e2 {tC} eC1 eC2
               let_bind_pairs
               (wf : @wff var1 var2 G t e1 e2)
               (H : forall (x1 : interp_flat_type var1 t) (x2 : interp_flat_type var2 t),
                   wff (flatten_binding_list x1 x2 ++ G) (eC1 (inl x1)) (eC2 (inl x2)))
               (H' : forall G' (x y : exprf t),
                   wff (G' ++ G) x y
                   -> wff (G' ++ G) (eC1 (inr x)) (eC2 (inr y)))
               {struct e1}
        : @wff var1 var2 G tC (under_letsf' let_bind_op_args let_bind_pairs e1 eC1) (under_letsf' let_bind_op_args let_bind_pairs e2 eC2).
      Proof using Type.
        revert H.
        set (e1v := e1) in *.
        destruct e1 as [ | | ? ? ? args | tx ex tC0 eC0 | ? ex ? ey ];
          [ clear wff_under_letsf'
          | clear wff_under_letsf'
          | clear wff_under_letsf'
          | generalize (fun G => match e1v return match e1v with LetIn _ _ _ _ => _ | _ => _ end with
                                 | LetIn _ ex _ eC => wff_under_letsf' G _ ex
                                 | _ => I
                                 end);
            generalize (fun G => match e1v return match e1v with LetIn tx0 _ tC1 e0 => _ | _ => _ end with
                                 | LetIn _ ex tC' eC => fun x => wff_under_letsf' G tC' (eC x)
                                 | _ => I
                                 end);
            clear wff_under_letsf'
          | generalize (fun G => match e1v return match e1v with Pair _ _ _ _ => _ | _ => _ end with
                                 | Pair _ ex _ ey => wff_under_letsf' G _ ex
                                 | _ => I
                                 end);
            generalize (fun G => match e1v return match e1v with Pair _ _ _ _ => _ | _ => _ end with
                                 | Pair _ ex _ ey => wff_under_letsf' G _ ey
                                 | _ => I
                                 end);
            clear wff_under_letsf' ];
          subst e1v;
          cbv beta iota;
          (invert_one_expr e2 || destruct e2); intros; try break_innermost_match_step; try exact I; intros;
            inversion_wf;
            t_fin idtac.
      Qed.

      Lemma  wff_under_letsf G {t} e1 e2 {tC} eC1 eC2
             (wf : @wff var1 var2 G t e1 e2)
             (H' : forall G' (x y : exprf t),
                 wff (G' ++ G) x y
                 -> wff (G' ++ G) (eC1 x) (eC2 y))
        : @wff var1 var2 G tC (under_letsf let_bind_op_args e1 eC1) (under_letsf let_bind_op_args e2 eC2).
      Proof using Type.
        apply wff_under_letsf'; t_fin idtac.
      Qed.
    End gen1.

    Local Hint Resolve wff_under_letsf.
    Local Hint Constructors or.
    Local Hint Extern 1 => progress unfold List.In in *.
    Local Hint Resolve wff_in_impl_Proper.
    Local Hint Resolve wff_SmartVarf.

    Section gen2.
      Context (let_bind_op_args : bool).

      Lemma wff_linearizef_gen G {t} e1 e2
        : @wff var1 var2 G t e1 e2
          -> @wff var1 var2 G t (linearizef_gen let_bind_op_args e1) (linearizef_gen let_bind_op_args e2).
      Proof using Type.
        induction 1; t_fin ltac:(apply wff_under_letsf).
      Qed.

      Local Hint Resolve wff_linearizef_gen.

      Lemma wf_linearize_gen {t} e1 e2
        : @wf var1 var2 t e1 e2
          -> @wf var1 var2 t (linearize_gen let_bind_op_args e1) (linearize_gen let_bind_op_args e2).
      Proof using Type.
        destruct 1; constructor; auto.
      Qed.
    End gen2.
  End with_var.

  Section gen.
    Context (let_bind_op_args : bool).

    Lemma Wf_Linearize_gen {t} (e : Expr t) : Wf e -> Wf (Linearize_gen let_bind_op_args e).
    Proof using Type.
      intros wf var1 var2; apply wf_linearize_gen, wf.
    Qed.
  End gen.

  Definition wff_linearizef {var1 var2} G {t} e1 e2
    : @wff var1 var2 G t e1 e2
      -> @wff var1 var2 G t (linearizef e1) (linearizef e2)
    := wff_linearizef_gen _ G e1 e2.
  Definition wff_a_normalf {var1 var2} G {t} e1 e2
    : @wff var1 var2 G t e1 e2
      -> @wff var1 var2 G t (a_normalf e1) (a_normalf e2)
    := wff_linearizef_gen _ G e1 e2.

  Definition wf_linearize {var1 var2 t} e1 e2
    : @wf var1 var2 t e1 e2
      -> @wf var1 var2 t (linearize e1) (linearize e2)
    := wf_linearize_gen _ e1 e2.
  Definition wf_a_normal {var1 var2 t} e1 e2
    : @wf var1 var2 t e1 e2
      -> @wf var1 var2 t (a_normal e1) (a_normal e2)
    := wf_linearize_gen _ e1 e2.

  Definition Wf_Linearize {t} (e : Expr t) : Wf e -> Wf (Linearize e)
    := Wf_Linearize_gen _ e.
  Definition Wf_ANormal {t} (e : Expr t) : Wf e -> Wf (ANormal e)
    := Wf_Linearize_gen _ e.
End language.

Hint Resolve Wf_Linearize_gen Wf_Linearize Wf_ANormal : wf.


text:
Require Export euclidean__axioms.
Require Export lemma__3__7b.
Require Export lemma__betweennotequal.
Require Export lemma__extensionunique.
Require Export lemma__inequalitysymmetric.
Require Export logic.
Definition lemma__partnotequalwhole : forall A B C, (euclidean__axioms.BetS A B C) -> (~(euclidean__axioms.Cong A B A C)).
Proof.
intro A.
intro B.
intro C.
intro H.
assert (* Cut *) (euclidean__axioms.neq A B) as H0.
- assert (* Cut *) ((euclidean__axioms.neq B C) /\ ((euclidean__axioms.neq A B) /\ (euclidean__axioms.neq A C))) as H0.
-- apply (@lemma__betweennotequal.lemma__betweennotequal A B C H).
-- destruct H0 as [H1 H2].
destruct H2 as [H3 H4].
exact H3.
- assert (* Cut *) (euclidean__axioms.neq B A) as H1.
-- apply (@lemma__inequalitysymmetric.lemma__inequalitysymmetric A B H0).
-- assert (* Cut *) (exists D, euclidean__axioms.BetS B A D) as H2.
--- apply (@euclidean__axioms.postulate__Euclid2 B A H1).
--- destruct H2 as [D H3].
assert (* Cut *) (euclidean__axioms.BetS D A B) as H4.
---- apply (@euclidean__axioms.axiom__betweennesssymmetry B A D H3).
---- assert (* Cut *) (euclidean__axioms.BetS D A C) as H5.
----- apply (@lemma__3__7b.lemma__3__7b D A B C H4 H).
----- assert (* Cut *) (euclidean__axioms.neq B C) as H6.
------ assert (* Cut *) ((euclidean__axioms.neq B C) /\ ((euclidean__axioms.neq A B) /\ (euclidean__axioms.neq A C))) as H6.
------- apply (@lemma__betweennotequal.lemma__betweennotequal A B C H).
------- destruct H6 as [H7 H8].
destruct H8 as [H9 H10].
exact H7.
------ assert (* Cut *) (~(euclidean__axioms.Cong A B A C)) as H7.
------- intro H7.
assert (* Cut *) (B = C) as H8.
-------- apply (@lemma__extensionunique.lemma__extensionunique D A B C H4 H5 H7).
-------- apply (@H6 H8).
------- exact H7.
Qed.

author: Karnaj

repo: dktactgeo

save_path: github-repos/coq/Karnaj-dktactgeo


text:
Require Export VST.veric.rmaps.
Require Export RamifyCoq.lib.List_ext.
Require Export RamifyCoq.graph.graph_model.
Require Export RamifyCoq.CertiGC.GCGraph.
Require Export RamifyCoq.CertiGC.spatial_gcgraph.
Require Export RamifyCoq.CertiGC.env_graph_gc.
Require Export RamifyCoq.msl_ext.iter_sepcon.

Identity Coercion LGraph_LabeledGraph: LGraph >-> LabeledGraph.
Coercion pg_lg: LabeledGraph >-> PreGraph.

Definition init_data2byte (d: init_data) : byte :=
  match d with
  | Init_int8 m => Byte.repr (Int.intval m)
  | _ => Byte.one
  end.

Definition all_string_constants (sh: share) (gv: globals) : mpred :=
  cstring sh (map init_data2byte (gvar_init v___stringlit_1)) (gv ___stringlit_1) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_2)) (gv ___stringlit_2) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_3)) (gv ___stringlit_3) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_4)) (gv ___stringlit_4) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_5)) (gv ___stringlit_5) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_6)) (gv ___stringlit_6) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_7)) (gv ___stringlit_7) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_8)) (gv ___stringlit_8) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_9)) (gv ___stringlit_9) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_10)) (gv ___stringlit_10) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_11)) (gv ___stringlit_11) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_12)) (gv ___stringlit_12) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_13)) (gv ___stringlit_13) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_14)) (gv ___stringlit_14) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_15)) (gv ___stringlit_15) *
  cstring sh (map init_data2byte (gvar_init v___stringlit_16)) (gv ___stringlit_16).

Definition test_int_or_ptr_spec :=
 DECLARE _test_int_or_ptr
 WITH x : val
 PRE [ _x OF int_or_ptr_type ]
   PROP(valid_int_or_ptr x) LOCAL(temp _x x) SEP()
 POST [ tint ]
   PROP()
   LOCAL(temp ret_temp
          (Vint (Int.repr (match x with
                    | Vint _ => 1
                    | _ => 0
                    end))))
   SEP().

Definition int_or_ptr_to_int_spec :=
  DECLARE _int_or_ptr_to_int
  WITH x : val
  PRE [ _x OF int_or_ptr_type ]
    PROP(is_int I32 Signed x) LOCAL(temp _x x) SEP()
  POST [ tint ]
    PROP() LOCAL (temp ret_temp x) SEP().

Definition int_or_ptr_to_ptr_spec :=
  DECLARE _int_or_ptr_to_ptr
  WITH x : val
  PRE [ _x OF int_or_ptr_type ]
    PROP(isptr x) LOCAL(temp _x x) SEP()
  POST [ tptr tvoid ]
    PROP() LOCAL (temp ret_temp x) SEP().

Definition int_to_int_or_ptr_spec :=
  DECLARE _int_to_int_or_ptr
  WITH x : val
  PRE [ _x OF tint ]
    PROP(valid_int_or_ptr x)
    LOCAL(temp _x x) SEP()
  POST [ int_or_ptr_type ]
    PROP() LOCAL (temp ret_temp x) SEP().

Definition ptr_to_int_or_ptr_spec :=
  DECLARE _ptr_to_int_or_ptr
  WITH x : val
  PRE [ _x OF tptr tvoid ]
    PROP(valid_int_or_ptr x) LOCAL(temp _x x) SEP()
  POST [ int_or_ptr_type ]
    PROP() LOCAL (temp ret_temp x) SEP().

Definition Is_block_spec :=
  DECLARE _Is_block
  WITH x : val
  PRE [ _x OF int_or_ptr_type ]
    PROP(valid_int_or_ptr x) LOCAL(temp _x x) SEP()
  POST [ tint ]
    PROP()
    LOCAL(temp ret_temp
               (Vint (Int.repr (match x with
                                | Vptr _ _ => 1
                                | _ => 0
                                end))))
    SEP().

Definition abort_with_spec :=
  DECLARE _abort_with
  WITH s: val, str: list byte, sh: share
  PRE [ _s OF tptr tschar]
    PROP (readable_share sh) LOCAL (temp _s s) SEP (cstring sh str s)
  POST [ tvoid ]
    PROP (False) LOCAL() SEP().

Definition IS_FROM_TYPE :=
  ProdType (ProdType (ProdType
                        (ProdType (ConstType share) (ConstType val))
                        (ConstType Z)) (ConstType val)) Mpred.

Program Definition Is_from_spec :=
  DECLARE _Is_from
  TYPE IS_FROM_TYPE
  WITH sh: share, start : val, n: Z, v: val, P: mpred
  PRE [ _from_start OF (tptr int_or_ptr_type),
        _from_limit OF (tptr int_or_ptr_type),
        _v OF (tptr int_or_ptr_type)]
    PROP ()
    LOCAL (temp _from_start start; temp _from_limit (offset_val n start); temp _v v)
    SEP (weak_derives P (memory_block sh n start * TT) && emp;
         weak_derives P (valid_pointer v * TT) && emp; P)
  POST [tint]
    EX b: {v_in_range v start n} + {~ v_in_range v start n},
    PROP ()
    LOCAL (temp ret_temp (Vint (Int.repr (if b then 1 else 0))))
    SEP (P).
Next Obligation.
Proof.
  repeat intro.
  destruct x as ((((?, ?), ?), ?), ?); simpl.
  unfold PROPx, LOCALx, SEPx; simpl; rewrite !approx_andp; f_equal; f_equal.
  rewrite !sepcon_emp, ?approx_sepcon, ?approx_idem, ?approx_andp.
  f_equal; f_equal; [|f_equal]; rewrite derives_nonexpansive_l; reflexivity.
Qed.
Next Obligation.
Proof.
  repeat intro.
  destruct x as ((((?, ?), ?), ?), ?); simpl.
  rewrite !approx_exp. apply f_equal; extensionality t.
  unfold PROPx, LOCALx, SEPx; simpl; rewrite !approx_andp; f_equal; f_equal.
  rewrite !sepcon_emp, approx_idem. reflexivity.
Qed.

Definition forward_p_address
           (p: forward_p_type) (ti: val) (f_info: fun_info) (g: LGraph) :=
  match p with
  | inl root_index => field_address
                        thread_info_type
                        [ArraySubsc (Znth root_index (live_roots_indices f_info));
                           StructField _args] ti
  | inr (v, n) => offset_val (WORD_SIZE * n) (vertex_address g v)
  end.

Definition limit_address g t_info from :=
  offset_val (WORD_SIZE * gen_size t_info from) (gen_start g from).

Definition next_address t_info to :=
  field_address heap_type
                [StructField _next;
                   ArraySubsc (Z.of_nat to); StructField _spaces] (ti_heap_p t_info).

Definition forward_spec :=
  DECLARE _forward
  WITH rsh: share, sh: share, gv: globals, fi: val, ti: val,
       g: LGraph, t_info: thread_info, f_info: fun_info,
       roots : roots_t, outlier: outlier_t,
       from: nat, to: nat, depth: Z, forward_p: forward_p_type
  PRE [ _from_start OF (tptr int_or_ptr_type),
        _from_limit OF (tptr int_or_ptr_type),
        _next OF (tptr (tptr int_or_ptr_type)),
        _p OF (tptr int_or_ptr_type),
        _depth OF tint]
    PROP (readable_share rsh; writable_share sh;
          super_compatible (g, t_info, roots) f_info outlier;
          forward_p_compatible forward_p roots g from;
          forward_condition g t_info from to;
          0 <= depth <= Int.max_signed;
          from <> to)
    LOCAL (temp _from_start (gen_start g from);
           temp _from_limit (limit_address g t_info from);
           temp _next (next_address t_info to);
           temp _p (forward_p_address forward_p ti f_info g);
           temp _depth (Vint (Int.repr depth)))
    SEP (all_string_constants rsh gv;
         fun_info_rep rsh f_info fi;
         outlier_rep outlier;
         graph_rep g;
         thread_info_rep sh t_info ti)
  POST [tvoid]
    EX g': LGraph, EX t_info': thread_info, EX roots': roots_t,
    PROP (super_compatible (g', t_info', roots') f_info outlier;
          roots' = upd_roots from to forward_p g roots f_info;
          forward_relation from to (Z.to_nat depth)
                           (forward_p2forward_t forward_p roots g) g g';
          forward_condition g' t_info' from to;
          thread_info_relation t_info t_info')
    LOCAL ()
    SEP (all_string_constants rsh gv;
         fun_info_rep rsh f_info fi;
         outlier_rep outlier;
         graph_rep g';
         thread_info_rep sh t_info' ti).

Definition forward_roots_spec :=
  DECLARE _forward_roots
  WITH rsh: share, sh: share, gv: globals, fi: val, ti: val,
       g: LGraph, t_info: thread_info, f_info: fun_info,
       roots: roots_t, outlier: outlier_t, from: nat, to: nat
  PRE [ _from_start OF (tptr int_or_ptr_type),
        _from_limit OF (tptr int_or_ptr_type),
        _next OF (tptr (tptr int_or_ptr_type)),
        _fi OF (tptr tuint),
        _ti OF (tptr thread_info_type)]
    PROP (readable_share rsh; writable_share sh;
          super_compatible (g, t_info, roots) f_info outlier;
          forward_condition g t_info from to;
          from <> to)
    LOCAL (temp _from_start (gen_start g from);
           temp _from_limit (limit_address g t_info from);
           temp _next (next_address t_info to);
           temp _fi fi; temp _ti ti)
    SEP (all_string_constants rsh gv;
         fun_info_rep rsh f_info fi;
         outlier_rep outlier;
         graph_rep g;
         thread_info_rep sh t_info ti)
  POST [tvoid]
    EX g' : LGraph, EX t_info': thread_info, EX roots': roots_t,
    PROP (super_compatible (g', t_info', roots') f_info outlier;
          forward_roots_relation from to f_info roots g roots' g';
          forward_condition g' t_info' from to;
          thread_info_relation t_info t_info')
    LOCAL ()
    SEP (all_string_constants rsh gv;
         fun_info_rep rsh f_info fi;
         outlier_rep outlier;
         graph_rep g';
         thread_info_rep sh t_info' ti).

Definition do_scan_spec :=
  DECLARE _do_scan
  WITH rsh: share, sh: share, gv: globals, fi: val, ti: val,
       g: LGraph, t_info: thread_info, f_info: fun_info,
       roots : roots_t, outlier: outlier_t,
       from: nat, to: nat, to_index: nat
  PRE [ _from_start OF (tptr int_or_ptr_type),
        _from_limit OF (tptr int_or_ptr_type),
        _scan OF (tptr int_or_ptr_type),
        _next OF (tptr (tptr int_or_ptr_type))]
    PROP (readable_share rsh; writable_share sh;
          super_compatible (g, t_info, roots) f_info outlier;
          forward_condition g t_info from to;
          from <> to; closure_has_index g to to_index;
          0 < gen_size t_info to; gen_unmarked g to)
    LOCAL (temp _from_start (gen_start g from);
           temp _from_limit (limit_address g t_info from);
           temp _scan (offset_val (- WORD_SIZE) (vertex_address g (to, to_index)));
           temp _next (next_address t_info to))
    SEP (all_string_constants rsh gv;
         fun_info_rep rsh f_info fi;
         outlier_rep outlier;
         graph_rep g;
         thread_info_rep sh t_info ti)
  POST [tvoid]
    EX g': LGraph, EX t_info': thread_info,
    PROP (super_compatible (g', t_info', roots) f_info outlier;
          forward_condition g' t_info' from to;
          do_scan_relation from to to_index g g';
          thread_info_relation t_info t_info')
    LOCAL ()
    SEP (all_string_constants rsh gv;
         fun_info_rep rsh f_info fi;
         outlier_rep outlier;
         graph_rep g';
         thread_info_rep sh t_info' ti).

Definition do_generation_spec :=
  DECLARE _do_generation
  WITH rsh: share, sh: share, gv: globals, fi: val, ti: val,
       g: LGraph, t_info: thread_info, f_info: fun_info,
       roots: roots_t, outlier: outlier_t, from: nat, to: nat
  PRE [ _from OF (tptr space_type),
        _to OF (tptr space_type),
        _fi OF (tptr tuint),
        _ti OF (tptr thread_info_type)]
    PROP (readable_share rsh; writable_share sh;
          super_compatible (g, t_info, roots) f_info outlier;
          do_generation_condition g t_info roots f_info from to;
          from <> to)
    LOCAL (temp _from (space_address t_info from);
           temp _to (space_address t_info to);
           temp _fi fi; temp _ti ti)
    SEP (all_string_constants rsh gv;
         fun_info_rep rsh f_info fi;
         outlier_rep outlier;
         graph_rep g;
         thread_info_rep sh t_info ti)
  POST [tvoid]
    EX g' : LGraph, EX t_info': thread_info, EX roots': roots_t,
    PROP (super_compatible (g', t_info', roots') f_info outlier;
          thread_info_relation t_info t_info';
          do_generation_relation from to f_info roots roots' g g')
    LOCAL ()
    SEP (all_string_constants rsh gv;
         fun_info_rep rsh f_info fi;
         outlier_rep outlier;
         graph_rep g';
         thread_info_rep sh t_info' ti).

Definition create_space_spec :=
  DECLARE _create_space
  WITH sh: share, s: val, n: Z, gv: globals, rsh: share
  PRE [ _s OF (tptr space_type),
        _n OF tuint]
    PROP (writable_share sh;
          readable_share rsh;
          0 <= n < MAX_SPACE_SIZE)
    LOCAL (temp _s s; temp _n (Vint (Int.repr n)); gvars gv)
    SEP (mem_mgr gv; all_string_constants rsh gv; data_at_ sh space_type s)
  POST [tvoid]
    EX p: val,
    PROP () LOCAL ()
    SEP (mem_mgr gv; all_string_constants rsh gv;
         malloc_token Ews (tarray int_or_ptr_type n) p;
         data_at_ Ews (tarray int_or_ptr_type n) p;
         data_at sh space_type (p, (p, (offset_val (WORD_SIZE * n) p))) s).

Definition zero_triple: (val * (val * val)) := (nullval, (nullval, nullval)).

Definition create_heap_spec :=
  DECLARE _create_heap
  WITH sh: share, gv: globals
  PRE []
    PROP (readable_share sh)
    LOCAL (gvars gv)
    SEP (mem_mgr gv; all_string_constants sh gv)
  POST [tptr heap_type]
    EX h: val, EX p: val,
    PROP () LOCAL (temp ret_temp h)
    SEP (mem_mgr gv; all_string_constants sh gv; malloc_token Ews heap_type h;
         data_at Ews heap_type
                 ((p, (p, (offset_val (WORD_SIZE * NURSERY_SIZE) p)))
                    :: list_repeat (Z.to_nat (MAX_SPACES - 1)) zero_triple) h;
         malloc_token Ews (tarray int_or_ptr_type NURSERY_SIZE) p;
         data_at_ Ews (tarray int_or_ptr_type NURSERY_SIZE) p).

Definition make_tinfo_spec :=
  DECLARE _make_tinfo
  WITH sh: share, gv: globals
  PRE []
    PROP (readable_share sh)
    LOCAL (gvars gv)
    SEP (mem_mgr gv; all_string_constants sh gv)
  POST [tptr thread_info_type]
    EX t: val, EX h: val, EX p: val,
    PROP () LOCAL (temp ret_temp t)
    SEP (mem_mgr gv; all_string_constants sh gv;
         malloc_token Ews thread_info_type t;
         data_at Ews thread_info_type
                 (p, (offset_val (WORD_SIZE * NURSERY_SIZE) p,
                      (h, list_repeat (Z.to_nat MAX_ARGS) Vundef))) t;
         malloc_token Ews heap_type h;
         data_at Ews heap_type
                 ((p, (p, (offset_val (WORD_SIZE * NURSERY_SIZE) p)))
                    :: list_repeat (Z.to_nat (MAX_SPACES - 1)) zero_triple) h;
         malloc_token Ews (tarray int_or_ptr_type NURSERY_SIZE) p;
         data_at_ Ews (tarray int_or_ptr_type NURSERY_SIZE) p).

Definition resume_spec :=
  DECLARE _resume
  WITH rsh: share, sh: share, gv: globals, fi: val, ti: val,
       g: LGraph, t_info: thread_info, f_info: fun_info,
       roots : roots_t
  PRE [ _fi OF (tptr tuint),
        _ti OF (tptr thread_info_type)]
    PROP (readable_share rsh; writable_share sh;
          graph_thread_info_compatible g t_info;
          graph_gen_clear g O)
    LOCAL (temp _fi fi; temp _ti ti; gvars gv)
    SEP (all_string_constants rsh gv;
         fun_info_rep rsh f_info fi;
         graph_rep g;
         thread_info_rep sh t_info ti)
  POST [tvoid]
    PROP (fun_word_size f_info <= total_space (heap_head (ti_heap t_info)))
    LOCAL ()
    SEP (all_string_constants rsh gv;
         fun_info_rep rsh f_info fi;
         graph_rep g;
         before_gc_thread_info_rep sh t_info ti).

Definition garbage_collect_spec :=
  DECLARE _garbage_collect
  WITH rsh: share, sh: share, gv: globals, fi: val, ti: val,
       g: LGraph, t_info: thread_info, f_info: fun_info,
       roots : roots_t, outlier: outlier_t
  PRE [ _fi OF (tptr tuint),
        _ti OF (tptr thread_info_type)]
    PROP (readable_share rsh; writable_share sh;
          super_compatible (g, t_info, roots) f_info outlier;
          garbage_collect_condition g t_info roots f_info;
          safe_to_copy g)
    LOCAL (temp _fi fi; temp _ti ti; gvars gv)
    SEP (all_string_constants rsh gv;
         fun_info_rep rsh f_info fi;
         outlier_rep outlier;
         graph_rep g;
         before_gc_thread_info_rep sh t_info ti;
         ti_token_rep t_info)
  POST [tvoid]
    EX g': LGraph, EX t_info': thread_info, EX roots': roots_t,
    PROP (super_compatible (g', t_info', roots') f_info outlier;
          garbage_collect_relation f_info roots roots' g g';
          garbage_collect_condition g' t_info' roots' f_info;
          safe_to_copy g')
    LOCAL ()
    SEP (mem_mgr gv;
         all_string_constants rsh gv;
         fun_info_rep rsh f_info fi;
         outlier_rep outlier;
         graph_rep g';
         before_gc_thread_info_rep sh t_info' ti;
         ti_token_rep t_info').

Definition reset_heap_spec :=
  DECLARE _reset_heap
  WITH h: val
  PRE [ _h OF (tptr heap_type)]
    PROP () LOCAL (temp _h h) SEP ()
  POST [tvoid]
  PROP () LOCAL () SEP ().

Definition free_heap_spec :=
  DECLARE _free_heap
  WITH h: val
  PRE [ _h OF (tptr heap_type)]
    PROP () LOCAL (temp _h h) SEP ()
  POST [tvoid]
  PROP () LOCAL () SEP ().

Definition Gprog: funspecs :=
  ltac:(with_library prog
                     [test_int_or_ptr_spec;
                      int_or_ptr_to_int_spec;
                      int_or_ptr_to_ptr_spec;
                      int_to_int_or_ptr_spec;
                      ptr_to_int_or_ptr_spec;
                      Is_block_spec;
                      Is_from_spec;
                      abort_with_spec;
                      forward_spec;
                      forward_roots_spec;
                      do_scan_spec;
                      do_generation_spec;
                      create_space_spec;
                      create_heap_spec;
                      make_tinfo_spec;
                      resume_spec;
                      garbage_collect_spec;
                      reset_heap_spec;
                      free_heap_spec]).

repo: RamifyCoq


text:
From Categories Require Import Category.
From Categories Require Import Functor.
From Categories Require Import Functor_Ops.
From Categories Require Import Ext_Cons.Comma.
From Categories Require Import Coq_Cats.Type_Cat.Type_Cat.
From Categories Require Import Coq_Cats.Type_Cat.Complete.
From Categories Require Import Limits.Limit GenProd_Eq_Limits.
From Categories Require Import Archetypal.Discr.Discr.
From Categories Require Import Ext_Cons.Arrow.

From TLTT Require Import MLTT2.Overture.
From TLTT Require Import Strict_eq.

Require Import Reedy.Inverse.
Require Import Reedy.Overture.

Require Import FunctionalExtensionality.

Import SubCategory.

(* ref:def:reduced-coslice *)
(*  Definition 3.7 *)
(** We define the reduced coslice category as a full subcategory of
    non-identity arrows in Coslice. The coslice category is defined
    as an istance of more general comma category.*)
Definition ReducedCoslice (C : Category) (z : C) : Category
  := Full_SubCategory (CoSlice C z)
                      (λ (x : Comma_Obj _ _),
                       Π (p : z ≡ CMO_trg x),
                       not (Etransport (λ y, y ⟶ CMO_trg x) p (CMO_hom x) ≡ id)).

Notation "z // C" := (ReducedCoslice C z) (at level 70).

(* Projecting a "target" object, i.e. codomain of an arrow [z ⟶ c] *)
Definition rc_trg {C : Category} {z : C} (rc : z // C) : C := CMO_trg (projT1 rc).

(* Projecting the objects (which are the arrows [z ⟶ c] for some [c])
   of the reduced coslice category *)
Definition rc_obj {C : Category} {z : C} (rc : z // C)
  : z ⟶ rc_trg rc
  := CMO_hom (projT1 rc).

(** We define a forgetful functor by projecting objects and arrows from the reduced coslice *)
Definition forget (C : Category) (c : C) : (c // C) ⇒ C :=
    {| FO := λ (a : c // C), CMO_trg (projT1 a);
       FA := λ (a b : c // C) (f : a ⟶ b), CMH_right (proj1_sig f);
       F_id := λ a, eq_refl _;
       F_compose := λ a b c f g, eq_refl _ |}.

Notation "'Uˢ'" := Type_Cat.

Section MatchingObject.

  Import Limit.
  Import Const_Func.
  Import Arrow.

  Open Scope object_scope.
  Open Scope morphism_scope.
  Open Scope category_scope.

  Definition get_tip {C D : Category} {F : C ⇒ D} (L : Limit F) := cone_apex (LRKE L).

  (* We define the matching object to be a "tip" of the limit cone of the
     composition of functors [X ∘ (forget C z)].
     The limit is defined through the local right Kan extension. We apply projected cone tip
     to [tt : unit] to obtain a required pretype.
   *)
  Definition matching_object `{InvCat} (X : C ⇒ Uˢ) (z : C) : Uˢ
    := (get_tip (LimitOf (X ∘ (forget C z)))) _o tt.

  Lemma limit_cone_nat_transf_iff {C : Category} (X : C ⇒ Uˢ) (z : C) :
    (get_tip (LimitOf X) _o tt) <-> NatTrans (@Const_Func C Uˢ 1) X.
  Proof.
    split.
    - intros L. destruct L as [prod_cone eqls]. simpl in *.
      refine {| Trans := _; Trans_com := _; Trans_com_sym := _|}.
      unfold Projs, D_imgs in *. simpl in *.
      Unshelve. Focus 3.
      refine (λ c uu, prod_cone c).

      intros c c' h.
      apply functional_extensionality. intros x. simpl.
      apply (Ehapply_dep eqls (Build_Arrow _ _ _ h)).

      intros c c' h. apply functional_extensionality. intros x. simpl.
      apply (eq_sym (Ehapply_dep eqls (Build_Arrow _ _ _ h))).
    - intros NT. destruct NT as [η Nsq Nsq_sym].
      cbn in *.
      exists (λ c, η c tt).
      apply functional_extensionality_dep. intros f.
      destruct f. simpl.
      apply (Ehapply_dep (Nsq _ _ _) tt).
  Qed.
End MatchingObject.

author: CoqHott

repo: reedy

save_path: github-repos/coq/CoqHott-reedy


text:
From Coq Require Import Psatz.
From Equations Require Import Equations.

Inductive Pre := Pi : Pre -> Pre.

Fixpoint pre_size (p : Pre) : nat :=
  match p with
  | Pi τ => 1 + pre_size τ
  end.

Inductive InterpInput :=
| inp_ctx (Γp : nat)
| inp_ty (Γp : nat) (Γ : nat) (σp : Pre).

Definition measure_input (ii : InterpInput) : nat :=
  match ii with
  | inp_ctx Γp => Γp
  | inp_ty Γp Γ σp => Γp + pre_size σp
  end.

Equations? interp (ii : InterpInput) : nat by wf (measure_input ii) lt :=
  interp (inp_ty Γp Γ (Pi τp)) :=
    let piΓ := interp (inp_ctx Γp) in
    let τ := interp (inp_ty Γp piΓ τp) in
    0;
  interp _ := 0.
Proof. all: abstract lia. Defined.

Definition test := interp_elim.

repo: Coq-Equations


text:
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(** * Decidable setoid equality theory.

   Author: Matthieu Sozeau
   Institution: LRI, CNRS UMR 8623 - University Paris Sud
*)

Set Implicit Arguments.
Unset Strict Implicit.

Generalizable Variables A B .

Local Notation "'λ'  x .. y , t" := (fun x => .. (fun y => t) ..)
  (at level 200, x binder, y binder, right associativity).

(** Export notations. *)

Require Export Coq.Classes.SetoidClass.

(** The [DecidableSetoid] class asserts decidability of a [Setoid].
   It can be useful in proofs to reason more classically. *)

Require Import Coq.Logic.Decidable.

Class DecidableSetoid `(S : Setoid A) :=
  setoid_decidable : forall x y : A, decidable (x == y).

(** The [EqDec] class gives a decision procedure for a particular setoid
   equality. *)

Class EqDec `(S : Setoid A) :=
  equiv_dec : forall x y : A, { x == y } + { x =/= y }.

(** We define the [==] overloaded notation for deciding equality. It does not
   take precedence of [==] defined in the type scope, hence we can have both
   at the same time. *)

Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).

Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
  match x with
    | left H => @right _ _ H
    | right H => @left _ _ H
  end.

Require Import Coq.Program.Program.

Open Local Scope program_scope.

(** Invert the branches. *)

Program Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).

(** Overloaded notation for inequality. *)

Infix "=/=" := nequiv_dec (no associativity, at level 70).

(** Define boolean versions, losing the logical information. *)

Definition equiv_decb `{EqDec A} (x y : A) : bool :=
  if x == y then true else false.

Definition nequiv_decb `{EqDec A} (x y : A) : bool :=
  negb (equiv_decb x y).

Infix "==b" := equiv_decb (no associativity, at level 70).
Infix "<>b" := nequiv_decb (no associativity, at level 70).

(** Decidable leibniz equality instances. *)

Require Import Coq.Arith.Arith.

(** The equiv is burried inside the setoid, but we can recover
  it by specifying which setoid we're talking about. *)

Program Instance eq_setoid A : Setoid A | 10 :=
  { equiv := eq ; setoid_equiv := eq_equivalence }.

Program Instance nat_eq_eqdec : EqDec (eq_setoid nat) :=
  eq_nat_dec.

Require Import Coq.Bool.Bool.

Program Instance bool_eqdec : EqDec (eq_setoid bool) :=
  bool_dec.

Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
  λ x y, in_left.

  Next Obligation.
  Proof.
    destruct x ; destruct y.
    reflexivity.
  Qed.

Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : EqDec (eq_setoid (prod A B)) :=
  λ x y,
    let '(x1, x2) := x in
    let '(y1, y2) := y in
    if x1 == y1 then
      if x2 == y2 then in_left
      else in_right
    else in_right.

  Solve Obligations using unfold complement ; program_simpl.

(** Objects of function spaces with countable domains like bool
  have decidable equality. *)

Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) :=
  λ f g,
    if f true == g true then
      if f false == g false then in_left
      else in_right
    else in_right.

  Solve Obligations using try red ; unfold equiv, complement ; program_simpl.

  Next Obligation.
  Proof.
    extensionality x.
    destruct x ; auto.
  Qed.

repo: Coq-misc


text:
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(** * Decimal numbers *)

(** These numbers coded in base 10 will be used for parsing and printing
    other Coq numeral datatypes in an human-readable way.
    See the [Numeral Notation] command.
    We represent numbers in base 10 as lists of decimal digits,
    in big-endian order (most significant digit comes first). *)

Require Import Datatypes.

(** Unsigned integers are just lists of digits.
    For instance, ten is (D1 (D0 Nil)) *)

Inductive uint :=
 | Nil
 | D0 (_:uint)
 | D1 (_:uint)
 | D2 (_:uint)
 | D3 (_:uint)
 | D4 (_:uint)
 | D5 (_:uint)
 | D6 (_:uint)
 | D7 (_:uint)
 | D8 (_:uint)
 | D9 (_:uint).

(** [Nil] is the number terminator. Taken alone, it behaves as zero,
    but rather use [D0 Nil] instead, since this form will be denoted
    as [0], while [Nil] will be printed as [Nil]. *)

Notation zero := (D0 Nil).

(** For signed integers, we use two constructors [Pos] and [Neg]. *)

Variant int := Pos (d:uint) | Neg (d:uint).

(** For decimal numbers, we use two constructors [Decimal] and
    [DecimalExp], depending on whether or not they are given with an
    exponent (e.g., 1.02e+01). [i] is the integral part while [f] is
    the fractional part (beware that leading zeroes do matter). *)

Variant decimal :=
 | Decimal (i:int) (f:uint)
 | DecimalExp (i:int) (f:uint) (e:int).

Declare Scope dec_uint_scope.
Delimit Scope dec_uint_scope with uint.
Bind Scope dec_uint_scope with uint.

Declare Scope dec_int_scope.
Delimit Scope dec_int_scope with int.
Bind Scope dec_int_scope with int.

Register uint as num.uint.type.
Register int as num.int.type.
Register decimal as num.decimal.type.

Fixpoint nb_digits d :=
  match d with
  | Nil => O
  | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d =>
    S (nb_digits d)
  end.

(** This representation favors simplicity over canonicity.
    For normalizing numbers, we need to remove head zero digits,
    and choose our canonical representation of 0 (here [D0 Nil]
    for unsigned numbers and [Pos (D0 Nil)] for signed numbers). *)

(** [nzhead] removes all head zero digits *)

Fixpoint nzhead d :=
  match d with
  | D0 d => nzhead d
  | _ => d
  end.

(** [unorm] : normalization of unsigned integers *)

Definition unorm d :=
  match nzhead d with
  | Nil => zero
  | d => d
  end.

(** [norm] : normalization of signed integers *)

Definition norm d :=
  match d with
  | Pos d => Pos (unorm d)
  | Neg d =>
    match nzhead d with
    | Nil => Pos zero
    | d => Neg d
    end
  end.

(** A few easy operations. For more advanced computations, use the conversions
    with other Coq numeral datatypes (e.g. Z) and the operations on them. *)

Definition opp (d:int) :=
  match d with
  | Pos d => Neg d
  | Neg d => Pos d
  end.

(** For conversions with binary numbers, it is easier to operate
    on little-endian numbers. *)

Fixpoint revapp (d d' : uint) :=
  match d with
  | Nil => d'
  | D0 d => revapp d (D0 d')
  | D1 d => revapp d (D1 d')
  | D2 d => revapp d (D2 d')
  | D3 d => revapp d (D3 d')
  | D4 d => revapp d (D4 d')
  | D5 d => revapp d (D5 d')
  | D6 d => revapp d (D6 d')
  | D7 d => revapp d (D7 d')
  | D8 d => revapp d (D8 d')
  | D9 d => revapp d (D9 d')
  end.

Definition rev d := revapp d Nil.

Definition app d d' := revapp (rev d) d'.

Definition app_int d1 d2 :=
  match d1 with Pos d1 => Pos (app d1 d2) | Neg d1 => Neg (app d1 d2) end.

(** [nztail] removes all trailing zero digits and return both the
    result and the number of removed digits. *)

Definition nztail d :=
  let fix aux d_rev :=
    match d_rev with
    | D0 d_rev => let (r, n) := aux d_rev in pair r (S n)
    | _ => pair d_rev O
    end in
  let (r, n) := aux (rev d) in pair (rev r) n.

Definition nztail_int d :=
  match d with
  | Pos d => let (r, n) := nztail d in pair (Pos r) n
  | Neg d => let (r, n) := nztail d in pair (Neg r) n
  end.

Module Little.

(** Successor of little-endian numbers *)

Fixpoint succ d :=
  match d with
  | Nil => D1 Nil
  | D0 d => D1 d
  | D1 d => D2 d
  | D2 d => D3 d
  | D3 d => D4 d
  | D4 d => D5 d
  | D5 d => D6 d
  | D6 d => D7 d
  | D7 d => D8 d
  | D8 d => D9 d
  | D9 d => D0 (succ d)
  end.

(** Doubling little-endian numbers *)

Fixpoint double d :=
  match d with
  | Nil => Nil
  | D0 d => D0 (double d)
  | D1 d => D2 (double d)
  | D2 d => D4 (double d)
  | D3 d => D6 (double d)
  | D4 d => D8 (double d)
  | D5 d => D0 (succ_double d)
  | D6 d => D2 (succ_double d)
  | D7 d => D4 (succ_double d)
  | D8 d => D6 (succ_double d)
  | D9 d => D8 (succ_double d)
  end

with succ_double d :=
  match d with
  | Nil => D1 Nil
  | D0 d => D1 (double d)
  | D1 d => D3 (double d)
  | D2 d => D5 (double d)
  | D3 d => D7 (double d)
  | D4 d => D9 (double d)
  | D5 d => D1 (succ_double d)
  | D6 d => D3 (succ_double d)
  | D7 d => D5 (succ_double d)
  | D8 d => D7 (succ_double d)
  | D9 d => D9 (succ_double d)
  end.

End Little.

(** Pseudo-conversion functions used when declaring
    Numeral Notations on [uint] and [int]. *)

Definition uint_of_uint (i:uint) := i.
Definition int_of_int (i:int) := i.

repo: Universal-Algebra-in-HoTT