text:
Set Default Proof Using "Type".
Set Suggest Proof Using.

Class irisG  := IrisG { }.
Inductive val :=.

Definition wp_pre `{irisG} : val -> (val -> Prop) -> Prop := fun v Φ => Φ v.

Definition wp_def `{irisG} : val -> (val -> Prop) -> Prop := wp_pre.
Definition wp_aux `{irisG} : Prop. exact True. Qed.

Section wp.
Context `{irisG}.
Implicit Types Φ : val -> Prop.
Implicit Types e : val.

(* Weakest pre *)
Lemma wp_unfold e Φ :
  wp_def e Φ <-> wp_pre e Φ.
Proof. easy. Qed.
End wp.

author: Blaisorblade

repo: Coq-playground


text:
Require Import String.

Require Import coqfo.api.
Require Import coqfo.dec.
Require Import coqfo.finite.
Require Import coqfo.abstraction.
Require coqfo.transfo.

Require Extraction.

Require Import Coq.extraction.ExtrOcamlBasic.

Require Import extraction.ExtrOcamlString.
Extract Inlined Constant String.append => "(^)".
Extract Inlined Constant String.string_dec => "String.(=)".
Extract Inductive string => "string" [ """""" "(fun (a, b) -> (String.make 1 a) ^ b)"] "(fun e c s -> if String.(=) s """" then e else c s.[0] (String.sub s 1 (String.length s - 1)))".

Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))".

Extract Inductive sigT => "( * )" [ "" ].
Extract Inlined Constant projT1 => "fst".
Extract Inlined Constant projT2 => "snd".

Extraction Inline eq_dec dc_dec.
Extraction Inline dec.OneDec dec.isEq2_obligation_1 dec.PairDec_obligation_1.
Extraction Inline finite.asDec_obligation_1 finite.asDec abstraction.newPredDec_obligation_1.

Extraction "extract.ml" MLCervino transfo.Transfo.

author: grayswandyr

repo: cervino

save_path: github-repos/coq/grayswandyr-cervino


text:
(*

  Copyright 2014 Cornell University
  Copyright 2015 Cornell University

  This file is part of VPrl (the Verified Nuprl project).

  VPrl is free software: you can redistribute it and/or modify
  it under the terms of the GNU General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
  (at your option) any later version.

  VPrl is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  GNU General Public License for more details.

  You should have received a copy of the GNU General Public License
  along with VPrl.  If not, see <http://www.gnu.org/licenses/>.

  Website: http://nuprl.org/html/verification/
  Authors: Abhishek Anand & Vincent Rahli

*)

Require Import type_sys_useful.
Require Import dest_close.

Lemma eq_term_equals_per_ffatoms_eq_if {p} :
  forall lib (eqa1 eqa2 : per(p)) x,
    eq_term_equals eqa1 eqa2
    -> eq_term_equals
         (per_ffatoms_eq lib eqa1 x)
         (per_ffatoms_eq lib eqa2 x).
Proof.
  introv eqt.
  unfold eq_term_equals, per_ffatoms_eq; introv; split; intro k; exrepnd;
  dands; auto; exists y; dands; auto; apply eqt; auto.
Qed.

Lemma per_ffatoms_eq_symmetric {p} :
  forall lib (eq : per(p)) x t1 t2,
    term_equality_symmetric eq
    -> per_ffatoms_eq lib eq x t1 t2
    -> per_ffatoms_eq lib eq x t2 t1.
Proof.
  introv tes per.
  allunfold @per_ffatoms_eq; exrepnd; dands; allrw; try (complete sp).
  exists y; dands; auto.
Qed.

Lemma per_ffatoms_eq_transitive {p} :
  forall lib (eq : per(p)) x t1 t2 t3,
    term_equality_transitive eq
    -> per_ffatoms_eq lib eq x t1 t2
    -> per_ffatoms_eq lib eq x t2 t3
    -> per_ffatoms_eq lib eq x t1 t3.
Proof.
  introv tet per1 per2.
  allunfold @per_ffatoms_eq; exrepnd.
  dands; try (allrw; complete sp).
  exists y; dands; auto.
Qed.

Lemma per_ffatoms_eq_cequiv {p} :
  forall lib (eq : per(p)) x t1 t2,
    term_equality_respecting lib eq
    -> cequivc lib t1 t2
    -> per_ffatoms_eq lib eq x t1 t1
    -> per_ffatoms_eq lib eq x t1 t2.
Proof.
  introv res ceq per.
  allunfold @per_ffatoms_eq; repnd; dands; auto; spcast.
  apply cequivc_axiom in ceq; auto.
Qed.

Lemma cequiv_mk_ffatoms {p} :
  forall lib t t' T x,
    computes_to_value lib t (mk_free_from_atoms T x)
    -> cequiv lib t t'
    -> {T', x' : @NTerm p $
         computes_to_value lib t' (mk_free_from_atoms T' x')
         # cequiv lib T T'
         # cequiv lib x x'}.
Proof. prove_cequiv_mk.
Qed.

Lemma cequivc_mkc_ffatoms {p} :
  forall lib t t' T x,
    computes_to_valc lib t (mkc_free_from_atoms T x)
    -> cequivc lib t t'
    -> {T', x' : @CTerm p $
         computes_to_valc lib t' (mkc_free_from_atoms T' x')
         # cequivc lib T T'
         # cequivc lib x x'}.
Proof.
  unfold computes_to_valc, cequivc; intros; destruct_cterms; allsimpl.
  generalize (cequiv_mk_ffatoms lib x2 x1 x0 x); intro k.
  repeat (dest_imp k hyp); exrepnd.
  applydup @computes_to_value_isvalue in k0 as j.
  inversion j as [u isp v]; subst.
  allrw <- @isprogram_free_from_atoms_iff; repnd.
  exists (mk_cterm T' isp0) (mk_cterm x' isp); simpl; sp.
Qed.

Lemma cequivc_utoken {o} :
  forall lib t t' u,
    computes_to_valc lib t (mkc_utoken u)
    -> @cequivc o lib t t'
    -> computes_to_valc lib t' (mkc_utoken u).
Proof.
  introv comp ceq.
  allapply @computes_to_valc_to_valuec; allsimpl.
  apply @cequivc_canonical_form with (t' := t') in comp; sp.
  apply lblift_cequiv0 in p; subst; auto.
Qed.

Lemma per_ffatoms_eq_elt {o} :
  forall lib (eqa : per(o)) x1 x2,
    term_equality_symmetric eqa
    -> term_equality_transitive eqa
    -> eqa x1 x2
    -> (per_ffatoms_eq lib eqa x1) <=2=> (per_ffatoms_eq lib eqa x2).
Proof.
  introv sym trans eqxs.
  unfold per_ffatoms_eq; introv; split; introv k; exrepnd; dands; auto;
  exists y; dands; auto.
  apply (trans x2 x1 y); sp.
  apply (trans x1 x2 y); sp.
Qed.

Lemma close_type_system_ffatoms {p} :
  forall lib (ts : cts(p))
         T T'
         (eq : per)
         A1 A2 x1 x2
         eqa,
    type_system lib ts
    -> defines_only_universes lib ts
    -> computes_to_valc lib T (mkc_free_from_atoms A1 x1)
    -> computes_to_valc lib T' (mkc_free_from_atoms A2 x2)
    -> close lib ts A1 A2 eqa
    -> type_sys_props lib (close lib ts) A1 A2 eqa
    -> eqa x1 x2
    -> (eq <=2=> (per_ffatoms_eq lib eqa x1))
    -> per_ffatoms lib (close lib ts) T T' eq
    -> type_sys_props lib (close lib ts) T T' eq.
Proof.
  introv tysys dou c1 c2 cla reca eqxs eqiff; introv per.

  rw @type_sys_props_iff_type_sys_props3.
  prove_type_sys_props3 SCase; intros.

  - SCase "uniquely_valued".
    dclose_lr.

    + SSCase "CL_ffatoms".
      clear per.
      allunfold @per_ffatoms; exrepd.
      unfold eq_term_equals; intros.
      allrw.
      ccomputes_to_eqval.
      revert t1 t2; rw @fold_eq_term_equals.
      apply eq_term_equals_per_ffatoms_eq_if; auto.
      onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt dum.
      generalize (uv A3 eqa0); sp.

  - SCase "type_symmetric"; repdors; subst; dclose_lr;
    apply CL_ffatoms;
    clear per;
    allunfold @per_ffatoms; exrepd;
    unfold per_ffatoms;
    ccomputes_to_eqval.

    + exists A1 A3 x1 x3 eqa0; sp; spcast; sp.
      apply eq_term_equals_trans with (eq2 := eq); sp.
      apply eq_term_equals_sym; sp.

  - SCase "type_value_respecting"; repdors; subst;
    apply CL_ffatoms; unfold per_ffatoms.

    { (* 1 *)
      generalize (cequivc_mkc_ffatoms lib T T3 A1 x1); introv k; repeat (autodimp k hyp); exrepnd.
      exists A1 T'0 x1 x' eqa; sp; spcast; sp.
      { onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        generalize (tyvr A1 T'0); sp. }
      { onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        pose proof (tevr x1 x') as h; repeat (autodimp h hyp).
        eapply tet; eauto.
        spcast; auto. }
    }

    { (* 2 *)
      generalize (cequivc_mkc_ffatoms lib T' T3 A2 x2); introv k; repeat (autodimp k hyp); exrepnd.
      exists A2 T'0 x2 x' eqa; sp; spcast; sp.
      { onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        generalize (tyvr A2 T'0); sp. }
      { onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        pose proof (tevr x2 x') as h; repeat (autodimp h hyp).
        eapply tet; eauto.
        spcast; auto. }
      { onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        pose proof (per_ffatoms_eq_elt lib eqa x1 x2) as h; repeat (autodimp h hyp).
        eapply eq_term_equals_trans; eauto. }
    }

  - SCase "term_symmetric".
    unfold term_equality_symmetric; introv eqt.
    rw eqiff in eqt; rw eqiff.
    apply per_ffatoms_eq_symmetric; sp.
    onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt; sp.

  - SCase "term_transitive".
    unfold term_equality_transitive; introv eqt1 eqt2.
    rw eqiff in eqt1; rw eqiff in eqt2; rw eqiff.
    apply @per_ffatoms_eq_transitive with (t2 := t2); sp.
    onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt; sp.

  - SCase "term_value_respecting".
    unfold term_equality_respecting; introv eqt ceq.
    rw eqiff in eqt; rw eqiff.
    spcast.
    apply per_ffatoms_eq_cequiv; sp.
    onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt; sp.

  - SCase "type_gsymmetric".
    repdors; subst; split; sp; dclose_lr;
    apply CL_ffatoms;
    clear per;
    allunfold @per_ffatoms; exrepd;
    ccomputes_to_eqval;
    unfold per_partial.

    { (* 1 *)
      exists A3 A1 x3 x1 eqa0; sp; spcast; sp.
      { onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        generalize (tygs A1 A3 eqa0); intro k; repeat (autodimp k hyp).
        rw <- k; sp. }
      { onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt; auto.
        pose proof (uv A3 eqa0) as h; autodimp h hyp.
        apply h; apply h in e; auto. }
      { eapply eq_term_equals_trans; eauto.
        onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt; auto.
        pose proof (uv A3 eqa0) as h; autodimp h hyp.
        pose proof (eq_term_equals_per_ffatoms_eq_if lib eqa0 eqa x1) as h1.
        autodimp h1 hyp; [apply eq_term_equals_sym; auto|].
        eapply eq_term_equals_trans; eauto.
        pose proof (per_ffatoms_eq_elt lib eqa x1 x3) as h2; repeat (autodimp h2 hyp).
        apply h; auto.
        eapply eq_term_equals_trans; eauto.
        apply eq_term_equals_per_ffatoms_eq_if; auto. }
    }

    { (* 2 *)
      exists A1 A0 x1 x0 eqa0; sp; spcast; sp.
      { onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        generalize (tygs A1 A0 eqa0); intro k; repeat (autodimp k hyp).
        rw k; sp. }
      { onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt; auto.
        pose proof (tygs A1 A0 eqa0) as k; repeat (autodimp k hyp); apply k in c3; clear k.
        pose proof (uv A0 eqa0) as h; autodimp h hyp.
        apply h; apply h in e; auto. }
      { eapply eq_term_equals_trans; eauto.
        onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt; auto.
        pose proof (tygs A1 A0 eqa0) as k; repeat (autodimp k hyp); apply k in c3; clear k.
        pose proof (uv A0 eqa0) as h; autodimp h hyp.
        pose proof (eq_term_equals_per_ffatoms_eq_if lib eqa0 eqa x0) as h1.
        autodimp h1 hyp; [apply eq_term_equals_sym; auto|].
        eapply eq_term_equals_trans; eauto.
        pose proof (per_ffatoms_eq_elt lib eqa x0 x1) as h2; repeat (autodimp h2 hyp).
        apply h; auto.
        eapply eq_term_equals_trans; eauto.
        apply eq_term_equals_per_ffatoms_eq_if; auto. }
    }

  - SCase "type_gtransitive"; sp.

  - SCase "type_mtransitive".
    repdors; subst; dclose_lr;
    try (move_term_to_top (per_ffatoms lib (close lib ts) T T4 eq2));
    try (move_term_to_top (per_ffatoms lib (close lib ts) T' T4 eq2));
    allunfold @per_ffatoms; exrepd;
    ccomputes_to_eqval.

    + dands; apply CL_ffatoms; unfold per_ffatoms.

      * exists A4 A3 x4 x3 eqa1; sp; spcast; sp.
        onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        generalize (tymt A1 A4 A3 eqa1 eqa0); sp.

        onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        pose proof (tygs A1 A4 eqa1) as k; repeat (autodimp k hyp).
        apply k in c6.
        pose proof (uv A4 eqa1) as h1; autodimp h1 hyp.
        pose proof (uv A3 eqa0) as h2; autodimp h2 hyp.
        apply h1; apply h1 in e1; apply h2 in e.
        eapply tet; eauto.

      * exists A4 A3 x4 x3 eqa0; sp; spcast; sp.
        onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        generalize (tymt A1 A4 A3 eqa1 eqa0); sp.

        onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        pose proof (tygs A1 A4 eqa1) as k; repeat (autodimp k hyp).
        apply k in c6.
        pose proof (uv A4 eqa1) as h1; autodimp h1 hyp.
        pose proof (uv A3 eqa0) as h2; autodimp h2 hyp.
        apply h2; apply h1 in e1; apply h2 in e.
        eapply tet; eauto.

        onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        pose proof (tygs A1 A4 eqa1) as k; repeat (autodimp k hyp).
        apply k in c6.
        pose proof (uv A4 eqa1) as h1; autodimp h1 hyp.
        pose proof (uv A3 eqa0) as h2; autodimp h2 hyp.
        apply h1 in e1; apply h2 in e.
        eapply eq_term_equals_trans; eauto.
        apply per_ffatoms_eq_elt; auto.
        introv z; apply h2 in z; apply h2; auto.
        introv z1 z2; apply h2 in z1; apply h2 in z2; apply h2; auto.
        eapply tet; eauto.
        apply h2; eapply tet; eauto.

    + dands; apply CL_ffatoms; unfold per_ffatoms.

      * exists A4 A3 x4 x3 eqa1; sp; spcast; sp.
        onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        generalize (tymt A2 A4 A3 eqa1 eqa0); sp.

        onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        pose proof (tygs A2 A4 eqa1) as k; repeat (autodimp k hyp).
        apply k in c6.
        pose proof (uv A4 eqa1) as h1; autodimp h1 hyp.
        pose proof (uv A3 eqa0) as h2; autodimp h2 hyp.
        apply h1; apply h1 in e1; apply h2 in e.
        eapply tet; eauto.

      * exists A4 A3 x4 x3 eqa0; sp; spcast; sp.
        onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        generalize (tymt A2 A4 A3 eqa1 eqa0); sp.

        onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        pose proof (tygs A2 A4 eqa1) as k; repeat (autodimp k hyp).
        apply k in c6.
        pose proof (uv A4 eqa1) as h1; autodimp h1 hyp.
        pose proof (uv A3 eqa0) as h2; autodimp h2 hyp.
        apply h2; apply h1 in e1; apply h2 in e.
        eapply tet; eauto.

        onedtsp uv tys tyt tyst tyvr tes tet tevr tygs tygt tymt.
        pose proof (tygs A2 A4 eqa1) as k; repeat (autodimp k hyp).
        apply k in c6.
        pose proof (uv A4 eqa1) as h1; autodimp h1 hyp.
        pose proof (uv A3 eqa0) as h2; autodimp h2 hyp.
        apply h1 in e1; apply h2 in e.
        eapply eq_term_equals_trans; eauto.
        apply per_ffatoms_eq_elt; auto.
        introv z; apply h2 in z; apply h2; auto.
        introv z1 z2; apply h2 in z1; apply h2 in z2; apply h2; auto.
        eapply tet; eauto.
        apply h2; eapply tet; eauto.
Qed.

author: vrahli

repo: NuprlInCoq

save_path: github-repos/coq/vrahli-NuprlInCoq


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)         *)
(************************************************************************)

Require Import BinNat.
Local Open Scope N_scope.

(** Obsolete file, see [BinNat] now,
    only compatibility notations remain here. *)

Definition Pdiv_eucl a b := N.pos_div_eucl a (Npos b).

Definition Pdiv_eucl_correct a b :
  let (q,r) := Pdiv_eucl a b in Npos a = q * Npos b + r
 := N.pos_div_eucl_spec a (Npos b).

Lemma Pdiv_eucl_remainder a b :
  snd (Pdiv_eucl a b) < Npos b.
Proof. now apply (N.pos_div_eucl_remainder a (Npos b)). Qed.

Notation Ndiv_eucl := N.div_eucl (compat "8.7").
Notation Ndiv := N.div (compat "8.7").
Notation Nmod := N.modulo (only parsing).

Notation Ndiv_eucl_correct := N.div_eucl_spec (only parsing).
Notation Ndiv_mod_eq := N.div_mod' (only parsing).
Notation Nmod_lt := N.mod_lt (compat "8.7").

author: princeton-vl

repo: CoqGym

save_path: github-repos/coq/princeton-vl-CoqGym


text:
Require Import CodeDeps.
Require Import Ident.

Local Open Scope Z_scope.

Definition _addr := 1%positive.
Definition _g := 2%positive.
Definition _granule := 3%positive.
Definition _i := 4%positive.
Definition _lock := 5%positive.
Definition _ret := 6%positive.
Definition _t'1 := 7%positive.
Definition _t'2 := 8%positive.

Definition smc_granule_undelegate_body :=
  (Ssequence
    (Ssequence
      (Scall (Some _t'1)
        (Evar _find_lock_granule (Tfunction (Tcons tulong (Tcons tulong Tnil))
                                   (tptr Tvoid) cc_default))
        ((Etempvar _addr tulong) :: (Econst_int (Int.repr 1) tuint) :: nil))
      (Sset _g (Etempvar _t'1 (tptr Tvoid))))
    (Ssequence
      (Ssequence
        (Scall (Some _t'2)
          (Evar _is_null (Tfunction (Tcons (tptr Tvoid) Tnil) tuint cc_default))
          ((Etempvar _g (tptr Tvoid)) :: nil))
        (Sifthenelse (Ebinop Oeq (Etempvar _t'2 tuint)
                       (Econst_long (Int64.repr 0) tulong) tint)
          (Ssequence
            (Scall None
              (Evar _granule_undelegate_ops (Tfunction
                                              (Tcons
                                                (tptr Tvoid)
                                                (Tcons tulong Tnil)) tvoid
                                              cc_default))
              ((Etempvar _g (tptr Tvoid)) ::
               (Etempvar _addr tulong) :: nil))
            (Sset _ret (Econst_long (Int64.repr 0) tulong)))
          (Sset _ret (Econst_long (Int64.repr 1) tulong))))
      (Sreturn (Some (Etempvar _ret tulong)))))
.

Definition f_smc_granule_undelegate := {|
  fn_return := tulong;
  fn_callconv := cc_default;
  fn_params := ((_addr, tulong) :: nil);
  fn_vars := nil;
  fn_temps := ((_g, (tptr Tvoid)) :: (_ret, tulong) ::
               (_t'2, tuint) :: (_t'1, (tptr Tvoid)) ::
               nil);
  fn_body := smc_granule_undelegate_body
|}.

author: columbia


text:
Require config.
Require tt.
Require syntax.

Section Ptt.

Local Instance havePrecondition : config.Precondition := {| config.flagPrecondition := config.Yes |}.
Context `{configReflection : config.Reflection}.
Context `{configBinaryProdType : config.BinaryProdType}.
Context `{configProdEta : config.ProdEta}.
Context `{configUniverses : config.Universes}.
Context `{configPropType : config.PropType}.
Context `{configIdType : config.IdType}.
Context `{configIdEliminator : config.IdEliminator}.
Context `{configEmptyType : config.EmptyType}.
Context `{configUnitType : config.UnitType}.
Context `{configBoolType : config.BoolType}.
Context `{configProdType : config.ProdType}.
Context `{configSyntax : syntax.Syntax}.

Definition isctx := tt.isctx.
Definition issubst := tt.issubst.
Definition istype := tt.istype.
Definition isterm := tt.isterm.
Definition eqctx := tt.eqctx.
Definition eqsubst := tt.eqsubst.
Definition eqtype := tt.eqtype.
Definition eqterm := tt.eqterm.

End Ptt.

author: TheoWinterhalter

repo: formal-type-theory


text:
(** **********************************************************

Benedikt Ahrens, Chris Kapulkin, Mike Shulman

january 2013

************************************************************)

(** **********************************************************

Contents : Definition of opposite category and functor

************************************************************)

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.

Require Import UniMath.MoreFoundations.All.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.FunctorCategory.

Local Open Scope cat.

(** * The opposite precategory of a precategory *)

Definition opp_precat_ob_mor (C : precategory_ob_mor) : precategory_ob_mor :=
   tpair (λ ob : UU, ob -> ob -> UU) C (λ a b : C, C⟦b, a⟧ ).

Definition opp_precat_data (C : precategory_data) : precategory_data :=
  tpair _ _ (tpair _ (λ c : opp_precat_ob_mor C, identity c)
                     (λ (a b c : opp_precat_ob_mor C) f g, g · f)).

Definition is_precat_opp_precat_data (C : precategory) : is_precategory (opp_precat_data C)
  := ((λ a b, pr212 C b a),,(λ a b, pr112 C b a)),,
     ((λ a b c d f g h, pr222 C d c b a h g f),,(λ a b c d f g h, pr122 C d c b a h g f)).

Definition opp_precat (C : precategory) : precategory :=
  tpair _ (opp_precat_data C) (is_precat_opp_precat_data C).

Local Notation "C '^op'" := (opp_precat C) (at level 3, format "C ^op") : cat.

Goal ∏ C:precategory, C^op^op = C. reflexivity. Qed.

Definition opp_ob {C : precategory} (c : ob C) : ob C^op := c.

Definition rm_opp_ob {C : precategory} (cop : ob C^op) : ob C := cop.

Definition opp_mor {C : precategory} {b c : C} (f : C⟦b, c⟧) : C^op⟦c, b⟧ := f.

Definition rm_opp_mor {C : precategory} {b c : C} (f : C^op⟦c, b⟧) : C⟦b, c⟧ := f.

Definition oppositeCategory : category -> category
  := λ M, @tpair precategory has_homsets (opp_precat M) (λ A B, homset_property M (rm_opp_ob B) (rm_opp_ob A)).

Definition opp_mor_eq {C : precategory} {a b : C} {f g : a --> b} (e : opp_mor f = opp_mor g) :
  f = g := e.

Lemma opp_opp_precat_ob_mor (C : precategory_ob_mor) : C = opp_precat_ob_mor (opp_precat_ob_mor C).
Proof.
  reflexivity.
Defined.

Lemma opp_opp_precat_ob_mor_compute (C : precategory_ob_mor) :
  idpath _ = maponpaths precategory_id_comp (opp_opp_precat_ob_mor C).
Proof.
  reflexivity.
Defined.

Lemma opp_opp_precat_data (C : precategory_data) : C = opp_precat_data (opp_precat_data C).
Proof.
  reflexivity.
Defined.

Lemma opp_opp_precat (C : precategory) (hs : has_homsets C) : C = C^op^op.
Proof.
  use total2_paths_f.
  - apply opp_opp_precat_data.
  - apply (isaprop_is_precategory _ hs).
Qed.

Definition opp_is_iso {C : precategory} {a b : C} (f : a --> b) :
  @is_iso C a b f -> @is_iso C^op b a f.
Proof.
  intros H.
  set (T := is_z_iso_from_is_iso _ H).
  apply (is_iso_qinv (C:=C^op) _ (pr1 T)).
  split; [ apply (pr2 (pr2 T)) | apply (pr1 (pr2 T)) ].
Qed.

Definition iso_from_opp {C : precategory} {a b : C} (f : a --> b) :
  @is_iso C^op b a f → @is_iso C a b f.
Proof.
  intros H.
  set (T := is_z_iso_from_is_iso _ H).
  apply (is_iso_qinv (C:=C) _ (pr1 T)).
  split; [ apply (pr2 (pr2 T)) | apply (pr1 (pr2 T)) ].
Qed.

Definition opp_iso {C : precategory} {a b : C} : @iso C a b -> @iso C^op b a.
  intro f.
  exists (pr1 f).
  set (T := is_z_iso_from_is_iso _ (pr2 f)).
  apply (is_iso_qinv (C:=C^op) _ (pr1 T)).
  split; [ apply (pr2 (pr2 T)) | apply (pr1 (pr2 T)) ].
Defined.

Lemma opp_is_inverse_in_precat {C : precategory} {a b : C} {f : a --> b} {g : b --> a} :
  @is_inverse_in_precat C a b f g -> @is_inverse_in_precat (opp_precat C) a b g f.
Proof.
  intros H.
  use make_is_inverse_in_precat.
  - exact (is_inverse_in_precat1 H).
  - exact (is_inverse_in_precat2 H).
Defined.

Definition opp_is_z_isomorphism {C : precategory} {a b : C} (f : a --> b) :
  @is_z_isomorphism C a b f -> @is_z_isomorphism C^op b a f.
Proof.
  intros H.
  use make_is_z_isomorphism.
  - exact (is_z_isomorphism_mor H).
  - exact (opp_is_inverse_in_precat (is_inverse_in_precat_inv H)).
Defined.

Definition opp_z_iso {C : precategory} {a b : C} : @z_iso C a b -> @z_iso C^op b a.
Proof.
  intros H.
  use make_z_iso.
  - exact (z_iso_mor H).
  - exact (inv_from_z_iso H).
  - exact (opp_is_inverse_in_precat (is_inverse_in_precat_inv H)).
Defined.

Definition z_iso_from_opp {C : precategory} {a b : C} (f : a --> b) :
  @is_z_isomorphism C^op b a f → @is_z_isomorphism C a b f.
Proof.
  intros H.
  exists (pr1 H).
  split; [ apply (pr2 (pr2 H)) | apply (pr1 (pr2 H)) ].
Qed.

Lemma has_homsets_opp {C : precategory} (hsC : has_homsets C) : has_homsets C^op.
Proof. intros a b; apply hsC. Defined.

Definition op_cat (c : category) : category := (opp_precat c,, has_homsets_opp (homset_property c) ).

(** * The opposite functor *)

Definition functor_opp_data {C D : precategory} (F : functor C D) :
  functor_data C^op D^op :=
    tpair (fun F : C^op -> D^op => ∏ a b, C^op ⟦a, b⟧ -> D^op ⟦F a, F b⟧) F
          (fun (a b : C) (f : C⟦b, a⟧) => functor_on_morphisms F f).

Lemma is_functor_functor_opp {C D : precategory} (F : functor C D) :
  is_functor (functor_opp_data F).
Proof. split; intros.
  - unfold functor_idax; simpl.
    apply (functor_id F).
  - unfold functor_compax; simpl.
    intros.
    apply (functor_comp F).
Qed.

Definition functor_opp {C D : precategory} (F : functor C D) : functor C^op D^op :=
  tpair _ _ (is_functor_functor_opp F).

(** Properties of the opp functor *)

Section opp_functor_properties.

Variables C D : precategory.
Variable F : functor C D.

Lemma opp_functor_fully_faithful : fully_faithful F -> fully_faithful (functor_opp F).
Proof.
  intros HF a b.
  apply HF.
Defined.

Lemma opp_functor_essentially_surjective :
  essentially_surjective F -> essentially_surjective (functor_opp F).
Proof.
  intros HF d.
  set (TH := HF d).
  set (X:=@hinhuniv  (∑ a : C, z_iso (F a) d)).
  use (X _ _ TH).
  intro H. clear TH. clear X.
  apply hinhpr.
  destruct H as [a X].
  exists a. simpl in *.
  apply  opp_z_iso.
  apply (z_iso_inv_from_z_iso X).
Qed.

End opp_functor_properties.

Notation "C '^op'" := (opp_precat C) (at level 3, format "C ^op") : cat.

Lemma functor_opp_identity {C : precategory} (hsC : has_homsets C) :
  functor_opp (functor_identity C) = functor_identity C^op.
Proof. apply (functor_eq _ _ (has_homsets_opp hsC)); trivial. Qed.

Lemma functor_opp_composite {C D E : precategory} (F : functor C D) (G : functor D E)
  (hsE : has_homsets E) : functor_opp (functor_composite F G) =
                          functor_composite (functor_opp F) (functor_opp G).
Proof. apply (functor_eq _ _ (has_homsets_opp hsE)); trivial. Qed.

Definition from_opp_to_opp_opp (A C : precategory) (hsC : has_homsets C) :
  functor_data [A, C, hsC]^op [A^op, C^op, has_homsets_opp hsC].
Proof.
apply (tpair _ functor_opp).
simpl; intros F G α.
use tpair.
+ simpl; intro a; apply α.
+ abstract (intros a b f; simpl in *;
            apply pathsinv0, (nat_trans_ax α)).
Defined.

Lemma is_functor_from_opp_to_opp_opp (A C : precategory) (hsC : has_homsets C) :
  is_functor (from_opp_to_opp_opp A C hsC).
Proof.
split.
- now intro F; simpl; apply (nat_trans_eq (has_homsets_opp hsC)); simpl; intro a.
- now intros F G H α β; simpl; apply (nat_trans_eq (has_homsets_opp hsC)); simpl; intro a.
Qed.

Definition functor_from_opp_to_opp_opp (A C : precategory) (hsC : has_homsets C) :
  functor [A, C, hsC]^op [A^op, C^op, has_homsets_opp hsC] :=
    tpair _ _ (is_functor_from_opp_to_opp_opp A C hsC).

Definition from_opp_opp_to_opp (A C : precategory) (hsC : has_homsets C) :
  functor_data [A^op, C^op, has_homsets_opp hsC] [A, C, hsC]^op.
Proof.
use tpair; simpl.
- intro F.
  use tpair.
  + exists F.
    apply (λ a b f, # F f).
  + abstract (split; [ intro a; apply (functor_id F)
                     | intros a b c f g; apply (functor_comp F)]).
- intros F G α; exists α.
  abstract (intros a b f; apply pathsinv0, (nat_trans_ax α)).
Defined.

Lemma is_functor_from_opp_opp_to_opp (A C : precategory) (hsC : has_homsets C) :
  is_functor (from_opp_opp_to_opp A C hsC).
Proof.
split.
- now intro F; simpl; apply (nat_trans_eq hsC); intro a.
- now intros F G H α β; simpl; apply (nat_trans_eq hsC); intro a.
Qed.

Definition functor_from_opp_opp_to_opp (A C : precategory) (hsC : has_homsets C) :
  functor [A^op, C^op, has_homsets_opp hsC] [A, C, hsC]^op :=
    tpair _ _ (is_functor_from_opp_opp_to_opp A C hsC).

Definition op_nt {c d : category} {f g : functor c d} (a : nat_trans f g)
  : nat_trans (functor_opp g) (functor_opp f).
Proof.
  use tpair.
  - exact (λ c, a c).
  - abstract
      (intros x y h;
       apply (! (nat_trans_ax a _ _ _ ))).
Defined.

Lemma op_nt_is_z_iso {C D : category} {f g : functor C D} (a : nat_trans f g) (is : is_nat_z_iso a)
  : is_nat_z_iso (op_nt a).
Proof.
  intro c.
  use opp_is_z_isomorphism.
  exact (is c).
Defined.

Lemma op_nt_is_iso {C D : category} {f g : functor C D} (a : nat_trans f g) (is : is_nat_iso a) : is_nat_iso (op_nt a).
Proof.
  intro c.
  use opp_is_iso.
  exact (is c).
Defined.

(** It's univalent *)

Definition op_iso_is_cat_iso
           {C : category}
           (X Y : C^op)
  : @iso C Y X ≃ iso X Y.
Proof.
  use weqfibtototal.
  intro f.
  use weqimplimpl.
  - apply opp_is_iso.
  - apply iso_from_opp.
  - apply isaprop_is_iso.
  - apply isaprop_is_iso.
Defined.

Definition has_homsets_op (C : category) : has_homsets (C^op).
Proof.
  intros a b.
  apply C.
Defined.

Definition op_category (C : category) : category := make_category C^op (has_homsets_op C).

Definition op_z_iso_is_cat_z_iso
           {C : category}
           (X Y : C^op)
  : @z_iso C Y X ≃ z_iso X Y.
Proof.
  use weqfibtototal.
  intro f.
  use weqimplimpl.
  - apply opp_is_z_isomorphism.
  - apply z_iso_from_opp.
  - apply isaprop_is_z_isomorphism.
  - apply (isaprop_is_z_isomorphism(C:=op_category C)).
Defined.

Definition from_op_op_to_op (A C : category)
  : functor [op_category A, op_category C] (op_category [A,C])
  := tpair _ _ (is_functor_from_opp_opp_to_opp A C C).

Definition op_is_univalent (C : univalent_category)
  : is_univalent (op_category C).
Proof.
  intros X Y.
  use weqhomot.
  + exact ((op_z_iso_is_cat_z_iso X Y)
             ∘ make_weq (@idtoiso C Y X) (pr2( C) Y X)
             ∘ weqpathsinv0 _ _)%weq.
  + intros p.
    induction p ; cbn.
    apply subtypePath.
    * intro ; apply (isaprop_is_z_isomorphism(C:=op_category C)).
    * apply idpath.
Defined.

Definition op_unicat (C : univalent_category)
  : univalent_category
  := (op_category C ,, op_is_univalent C).

Notation "C '^op'" := (op_category C) (at level 3, format "C ^op") : cat.

Definition op_ob {C : category} (c : ob C) : ob C^op := c.

Definition rm_op_ob {C : category} (cop : ob C^op) : ob C := cop.

Definition op_mor {C : category} {b c : C} (f : C⟦b, c⟧) : C^op⟦c, b⟧ := f.

Definition rm_op_mor {C : category} {b c : C} (f : C^op⟦c, b⟧) : C⟦b, c⟧ := f.

(** Functoriality of taking the opposite *)
Definition functor_identity_op
           (C : category)
  : functor_identity (C^op)
    ⟹
    functor_opp (functor_identity C).
Proof.
  use make_nat_trans.
  - exact (λ x, identity x).
  - abstract
      (intros x y f ; cbn ;
       rewrite id_left, id_right ;
       apply idpath).
Defined.

Definition is_nat_z_iso_functor_identity_op
           (C : category)
  : is_nat_z_iso (functor_identity_op C).
Proof.
  intros x.
  apply is_z_isomorphism_identity.
Defined.

Definition functor_identity_op_nat_z_iso
           (C : category)
  : nat_z_iso
      (functor_identity (C^op))
      (functor_opp (functor_identity C)).
Proof.
  use make_nat_z_iso.
  - exact (functor_identity_op C).
  - exact (is_nat_z_iso_functor_identity_op C).
Defined.

Definition functor_comp_op
           {C₁ C₂ C₃ : category}
           (F : C₁ ⟶ C₂)
           (G : C₂ ⟶ C₃)
  : functor_opp F ∙ functor_opp G ⟹ functor_opp (F ∙ G).
Proof.
  use make_nat_trans.
  - exact (λ x, identity _).
  - abstract
      (intros x y f ; cbn ;
       rewrite id_left, id_right ;
       apply idpath).
Defined.

Definition is_nat_z_iso_functor_comp_op
           {C₁ C₂ C₃ : category}
           (F : C₁ ⟶ C₂)
           (G : C₂ ⟶ C₃)
  : is_nat_z_iso (functor_comp_op F G).
Proof.
  intros x.
  apply is_z_isomorphism_identity.
Defined.

Definition functor_comp_op_nat_z_iso
           {C₁ C₂ C₃ : category}
           (F : C₁ ⟶ C₂)
           (G : C₂ ⟶ C₃)
  : nat_z_iso
      (functor_opp F ∙ functor_opp G)
      (functor_opp (F ∙ G)).
Proof.
  use make_nat_z_iso.
  - exact (functor_comp_op F G).
  - exact (is_nat_z_iso_functor_comp_op F G).
Defined.

(** It forms a duality involution *)
Definition op_unit_nat_trans
           {C₁ C₂ : category}
           (F : C₁ ⟶ C₂)
  : functor_identity _ ∙ functor_opp (functor_opp F)
    ⟹
    F ∙ functor_identity _.
Proof.
  use make_nat_trans.
  - exact (λ x, identity (F x)).
  - abstract
      (intros x y f ; cbn ;
       rewrite id_left, id_right ;
       apply idpath).
Defined.

Definition op_unit_nat_z_iso
           {C₁ C₂ : category}
           (F : C₁ ⟶ C₂)
  : nat_z_iso
      (functor_identity _ ∙ functor_opp (functor_opp F))
      (F ∙ functor_identity _).
Proof.
  use make_nat_z_iso.
  - exact (op_unit_nat_trans F).
  - intro.
    apply identity_is_z_iso.
Defined.

Definition op_unit_inv_nat_trans
           {C₁ C₂ : category}
           (F : C₁ ⟶ C₂)
  : functor_identity _ ∙ F
    ⟹
    functor_opp (functor_opp F) ∙ functor_identity _.
Proof.
  use make_nat_trans.
  - exact (λ x, identity (F x)).
  - abstract
      (intros x y f ; cbn ;
       rewrite id_left, id_right ;
       apply idpath).
Defined.

Definition op_unit_inv_nat_z_iso
           {C₁ C₂ : category}
           (F : C₁ ⟶ C₂)
  : nat_z_iso
      (functor_identity _ ∙ F)
      (functor_opp (functor_opp F) ∙ functor_identity _).
Proof.
  use make_nat_z_iso.
  - exact (op_unit_inv_nat_trans F).
  - intro.
    apply identity_is_z_iso.
Defined.

Definition op_triangle_nat_trans
           (C : category)
  : functor_identity _ ⟹ functor_opp (functor_identity C).
Proof.
  use make_nat_trans.
  - exact (λ x, identity x).
  - abstract
      (intros x y f ; cbn ;
       rewrite id_left, id_right ;
       apply idpath).
Defined.

Definition op_triangle_nat_z_iso
           (C : category)
  : nat_z_iso
      (functor_identity _)
      (functor_opp (functor_identity C)).
Proof.
  use make_nat_z_iso.
  - exact (op_triangle_nat_trans C).
  - intro.
    apply identity_is_z_iso.
Defined.

Definition op_unit_unit_inv_nat_trans
           (C : category)
  : nat_trans
      (functor_identity C)
      (functor_identity C ∙ functor_identity ((C^op)^op)).
Proof.
  use make_nat_trans.
  - exact (λ x, identity x).
  - abstract
      (intros x y f ; cbn ;
       rewrite id_left, id_right ;
       apply idpath).
Defined.

Definition op_unit_unit_inv_nat_z_iso
           (C : category)
  : nat_z_iso
      (functor_identity C)
      (functor_identity C ∙ functor_identity ((C^op)^op)).
Proof.
  use make_nat_z_iso.
  - exact (op_unit_unit_inv_nat_trans C).
  - intro.
    apply identity_is_z_iso.
Defined.

Definition op_unit_inv_unit_nat_trans
           (C : category)
  : nat_trans
      (functor_identity ((C^op)^op) ∙ functor_identity C)
      (functor_identity ((C^op)^op)).
Proof.
  use make_nat_trans.
  - exact (λ x, identity x).
  - abstract
      (intros x y f ; cbn ;
       rewrite id_left, id_right ;
       apply idpath).
Defined.

Definition op_unit_inv_unit_nat_z_iso
           (C : category)
  : nat_z_iso
      (functor_identity ((C^op)^op) ∙ functor_identity C)
      (functor_identity ((C^op)^op)).
Proof.
  use make_nat_z_iso.
  - exact (op_unit_inv_unit_nat_trans C).
  - intro.
    apply identity_is_z_iso.
Defined.

author: UniMath

repo: UniMath

save_path: github-repos/coq/UniMath-UniMath


text:
Require Import Coq.Lists.List.
Import ListNotations.
Require Import riscv.Program.
Require Import riscv.Decode.
Require Import riscv.util.BitWidth32.
Require Import bbv.HexNotationZ.
Require Import Coq.ZArith.BinInt.
Require Import riscv.Utility.
Require Import riscv.Memory.
Require Import riscv.Minimal.
Require Import riscv.MinimalLogging.
Require Import riscv.Run.
Require Import riscv.ListMemory.
Require Import riscv.util.Monads.
Require Import riscv.MachineWidth32.

Existing Instance DefaultRiscvState.

Instance FunctionRegisterFile: RegisterFile (Register -> word 32) Register (word 32) := {|
  getReg(rf: Register -> word 32) := rf;
  setReg(rf: Register -> word 32)(r: Register)(v: word 32) :=
    fun r' => if (Z.eqb r' r) then v else rf r';
  initialRegs := fun r => ZToReg 0;
|}.

Definition fib6_riscv: list MachineInt := [ (* TODO should be "word 32", not MachineInt *)
  Ox"00600993";         (* li s3,6 *)
  Ox"00000a13";         (* li s4,0 *)
  Ox"00100913";         (* li s2,1 *)
  Ox"00000493";         (* li s1,0 *)
  Ox"0140006f";         (* j 101e0 <main+0x44> *)
  Ox"012a0ab3";         (* add s5,s4,s2 *)
  Ox"00090a13";         (* mv s4,s2 *)
  Ox"000a8913";         (* mv s2,s5 *)
  Ox"00148493";         (* addi s1,s1,1 *)
  Ox"ff34c8e3"          (* blt s1,s3,101d0 <main+0x34> *)
].

(*
Notation x0 := (WO~0~0~0~0~0)%word.
Notation s1 := (WO~0~1~0~0~1)%word.
Notation s2 := (WO~1~0~0~1~0)%word.
Notation s3 := (WO~1~0~0~1~1)%word.
Notation s4 := (WO~1~0~1~0~0)%word.
Notation s5 := (WO~1~0~1~0~1)%word.
*)

Open Scope Z_scope.

Goal False.
  set (l := map (decode RV32IM) fib6_riscv).
  cbv in l.
  (* decoder seems to work :) *)
Abort.

Definition RiscvMachine := @RiscvMachine (word 32) mem (Register -> word 32).

(* This example uses the memory only as instruction memory
   TODO make an example which uses memory to store data *)
Definition zeroedRiscvMachineCore: RiscvMachineCore := {|
  registers := initialRegs;
  pc := ZToReg 0;
  nextPC := ZToReg 4;
  exceptionHandlerAddr := 3;
|}.

Definition zeroedRiscvMachine: RiscvMachine := {|
    core := zeroedRiscvMachineCore;
    machineMem := zero_mem 100;
|}.

Definition zeroedRiscvMachineL: RiscvMachineL := {|
    machine := zeroedRiscvMachine;
    log := nil;
|}.

Definition initialRiscvMachineL(imem: list MachineInt): RiscvMachineL :=
  putProgram (map (@ZToWord 32) imem) (ZToReg 0) zeroedRiscvMachineL.

Definition run: nat -> RiscvMachineL -> (option unit) * RiscvMachineL := run.
 (* @run BitWidths32 MachineWidth32 (OState RiscvMachineL) (OState_Monad _) _ _ _ *)

Definition fib6_L_final(fuel: nat): RiscvMachineL :=
  match run fuel (initialRiscvMachineL fib6_riscv) with
  | (answer, state) => state
  end.

Definition fib6_L_res(fuel: nat): word XLEN :=
  (fib6_L_final fuel).(machine).(core).(registers) 18.

Definition fib6_L_trace(fuel: nat): Log :=
  (fib6_L_final fuel).(log).

(* only uncomment this if you're sure there are no admits in the computational parts,
   otherwise this will eat all your memory *)

Eval cbv in (fib6_L_trace 50).

Lemma fib6_res_is_13_by_running_it: exists fuel, fib6_L_res fuel = ZToReg 13.
  exists 50%nat.
  reflexivity.
Qed.

author: samuelgruetter

repo: riscv-coq


text:
(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)

(** %\subsection*{ support :  seq\_set\_seq.v }%*)
Set Implicit Arguments.
Unset Strict Implicit.
Require Export seq_set.

(** - Suppose we have a sequence $a=\langle a_0,...,a_{n-1}\rangle$ of elements of
 Setoid A. We can make a Setoid out of those: $\{a_0...a_{n-1}\}$, ie. (seq_set a)
 Now the original sequence a "is" also a sequence of elements of this new Setoid
 This "new" sequence (ie. the old one in a new guise) is (seq_set_seq a) *)

Let seq_set_fun :
  forall (A : Setoid) (n : Nat) (v : seq n A), fin n -> (seq_set v:Type).
intros.
apply (Build_subtype (P:=seq_set v:Predicate _) (subtype_elt:=v X)).
simpl in |- *.
exists X.
apply Refl.
Defined.

(** %\label{seqsetseq}% *)
Definition seq_set_seq :
  forall (A : Setoid) (n : Nat) (v : seq n A), seq n (seq_set v).
intros.
simpl in |- *.
apply (Build_Map (Ap:=seq_set_fun v)).
red in |- *.
intros.
simpl in |- *.
red in |- *.
simpl in |- *.
apply Ap_comp; auto with algebra.
Defined.

author: coq-contribs

repo: lin-alg

save_path: github-repos/coq/coq-contribs-lin-alg


text:
(***********************************************************************
      Div.v

      Definition of division and modulo

      Definitions: div mod

                                     Laurent.Thery@inria.fr (2006)
************************************************************************)
Require Import Arith.
Require Import Tactic.

Fixpoint div_aux (n m1 m2 p: nat) {struct n}: nat :=
  match m1 with
    O =>
       match p with
            O => 1
       | S p1 =>
         match n with
           0 => 0 (* impossible *)
         | S n1 => S (div_aux n1 m2 m2 p1)
         end
       end
   | S m =>
       match p with
        O => 0
       | S p1  =>
         match n with
           0 => 0 (* impossible *)
         | S n1 => div_aux n1 m m2 p1
         end
       end
  end.

Definition div n m := match m with O => O | S m1 => div_aux n m m1 n end.

Fixpoint mod_aux (n m1 m2 p r: nat) {struct n}: nat :=
  match m1 with
    O =>
       match p with
            O => 0
       | S p1 =>
         match n with
           0 => 0 (* impossible *)
         | S n1 => (mod_aux n1 m2 m2 p1 p)
         end
       end
   | S m =>
       match p with
        O => r
       | S p1  =>
         match n with
           0 => 0 (* impossible *)
         | S n1 => mod_aux n1 m m2 p1 r
         end
       end
  end.

Theorem div_mod_aux_correct n m1 m2 p r :
   p <= n -> m1 <= S m2 -> r + m1 = p + S m2 ->
   div_aux n m1 m2 p * (S m2) + m1 + mod_aux n m1 m2 p r = p + (S m2).
Proof.
revert m1 m2 p r; elim n; simpl; auto.
  intros m1 m2 p r; case p.
    intros _; case m1; auto with arith.
      rewrite mult_1_l; rewrite plus_0_l; rewrite plus_0_r; auto with arith.
      intros p1; repeat (rewrite mult_0_l || rewrite plus_0_l
                                          || rewrite plus_0_r); auto.
    intros p1; repeat (rewrite mult_0_l || rewrite plus_0_l
                                        || rewrite plus_0_r); auto.
    intros _ H; rewrite <- H; auto with arith.
  intros n1 H; contradict H; auto with arith.
intros n1 Rec m1 m2 p; case m1; case p;
 repeat (rewrite mult_1_l || rewrite plus_0_l || rewrite plus_0_r);
 auto with arith.
- intros p1 r H1 H2 H3.
  match goal with |- ?X = ?Y =>
    replace X with (S ((div_aux n1 m2 m2 p1) * S m2 + m2 + mod_aux n1 m2 m2 p1 (S p1)));
    replace Y with (S (p1 + S m2))
  end; auto with arith.
    eq_tac; auto with arith.
    apply Rec; auto with arith.
    rewrite <- plus_n_Sm; auto.
  simpl; rewrite plus_0_r; eq_tac; auto with arith.
- intros m r _ _ H; rewrite <- H; auto with arith.
- intros p1 m r H H1 H2.
  match goal with |- ?X = ?Y =>
    replace X with (S (div_aux n1 m m2 p1 * S m2 + m + mod_aux n1 m m2 p1 r));
    replace Y with (S (p1 + S m2))
  end; auto with arith.
    eq_tac; auto with arith.
    apply Rec; auto with arith.
    apply eq_add_S.
    simpl in H2; rewrite <- H2.
    rewrite <- plus_n_Sm; auto.
  rewrite <- plus_n_Sm; auto.
Qed.

Theorem mod_aux_lt n m1 m2 p r :
 p <= n -> m1 <= S m2 -> r + m1 = p + S m2 ->
   mod_aux n m1 m2 p r < (S m2).
Proof.
revert m1 m2 p r; elim n; simpl; auto.
  intros m1 m2 p r; case p.
    intros _; case m1; auto with arith.
    intros m _ H; rewrite plus_0_l in H; rewrite <- H; auto with arith.
    apply le_lt_trans with (r + 0); auto with arith.
  intros n1 H; contradict H; auto with arith.
intros n1 Rec m1 m2 p; case m1; case p;
    repeat (rewrite mult_1_l || rewrite plus_0_l || rewrite plus_0_r);
    auto with arith.
- intros p1 r H1 H2 H3; apply Rec; auto with arith.
  rewrite <- plus_n_Sm; auto.
- intros m r _ _ H; rewrite <- H; auto with arith.
  apply le_lt_trans with (r + 0); auto with arith.
- intros p1 m r H H1 H2.
  apply Rec; auto with arith.
  apply eq_add_S.
  rewrite plus_n_Sm; auto.
Qed.

Definition modn n m := match m with O => O | S m1 => mod_aux n m m1 n n end.

Theorem div_mod_correct n m : 0 < m -> n = div n m * m + modn n m.
Proof.
case m; simpl; auto with arith.
  intros H; contradict H; auto with arith.
intros m1 H.
apply plus_reg_l with (S m1).
repeat rewrite (plus_comm (S m1)).
rewrite <- (div_mod_aux_correct n (S m1) m1 n n); auto with arith.
repeat rewrite <- plus_assoc; auto with arith.
Qed.

Theorem mod_lt n m : 0 < m -> modn n m < m.
Proof.
case m; simpl; auto with arith.
intros m1 H; apply mod_aux_lt; auto with arith.
Qed.

Theorem div_lt a b c : a < b * c -> div a b < c.
Proof.
intro H; rewrite (div_mod_correct a b) in H.
  case (le_or_lt c (div a b)); auto; intros H1; contradict H.
  apply le_not_lt.
  apply le_trans with (b * (div a b) + 0); auto with arith.
  rewrite (mult_comm b); auto with arith.
generalize H; case b; auto with arith.
intros H1; contradict H1; auto with arith.
Qed.

Theorem div_is_0 n m : n < m -> div n m = 0.
Proof.
intro H; assert (div n m < 1); auto with arith.
  apply div_lt; auto with arith.
  rewrite mult_1_r; auto with arith.
generalize H0; case (div n m); auto with arith.
intros n1 H1; contradict H1; apply le_not_lt; auto with arith.
Qed.

Theorem mult_lt_plus a b c d : a < b -> c < d -> a * d + c < b * d.
Proof.
intros HH HH1.
apply lt_le_trans with ((S a) * d); auto with arith.
  simpl; rewrite plus_comm; auto with arith.
apply mult_le_compat_r; auto with arith.
Qed.

Theorem lexico_mult a1 a2 b c1 c2 :
  c1 < b -> c2 < b -> a1 * b + c1 = a2 * b + c2 -> a1 = a2.
Proof.
intros H1 H2 H3.
case (le_or_lt a1 a2); intros H4.
  case le_lt_or_eq with (1 := H4); auto; clear H4; intros H4.
  absurd (a1 * b + c1 < a2 * b + c2); auto with arith.
    rewrite H3; auto with arith.
  apply lt_le_trans with ((S a1) * b + 0); auto with arith.
    rewrite plus_0_r; simpl; rewrite (plus_comm b); auto with arith.
  apply plus_le_compat; auto with arith.
  apply mult_le_compat_r; auto with arith.
absurd (a2 * b + c2 < a1 * b + c1); auto with arith.
rewrite H3; auto with arith.
apply lt_le_trans with ((S a2) * b + 0); auto with arith.
  rewrite plus_0_r; simpl; rewrite (plus_comm b); auto with arith.
apply plus_le_compat; auto with arith.
apply mult_le_compat_r; auto with arith.
Qed.

Theorem div_mult_comp n m p : 0 < p ->  div (p * m + n) p = m + div n p.
Proof.
intros H0; apply lexico_mult with (b := p) (c1 := modn (p * m + n) p) (c2 := modn n p);
  try apply mod_lt; auto with arith.
rewrite mult_plus_distr_r; rewrite <- plus_assoc;
  repeat rewrite <- div_mod_correct; auto with arith.
Qed.

Theorem mod_small n m : n < m -> modn n m = n.
Proof.
intros H; pattern n at 2; rewrite (div_mod_correct n m).
  rewrite div_is_0; auto.
apply le_lt_trans with (2 := H); auto with arith.
Qed.

Theorem mod_mult_comp n m p : 0 < p ->  modn (p * m + n) p = modn n p.
Proof.
intros H; apply plus_reg_l with (div (p * m + n) p * p).
rewrite <- div_mod_correct; auto.
rewrite div_mult_comp; auto.
rewrite mult_plus_distr_r; rewrite (mult_comm p); rewrite <- plus_assoc.
eq_tac; apply div_mod_correct; auto.
Qed.

author: thery

repo: sudoku

save_path: github-repos/coq/thery-sudoku


text:
(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)

(**
   pock.
   Pocklington's criterion.

   @author Olga Caprotti and Martijn Oostdijk
   @version $Revision$
*)

Require Import Arith.
Require Import ZArith.

Require Import lemmas.
Require Import natZ.
Require Import dec.
Require Import list.
Require Import exp.
Require Import divides.
Require Import prime.
Require Import modulo.
Require Import gcd.
Require Import modprime.
Require Import order.

(**
   For all numbers q in natlist qlist: 1 is a linear combination
   of a^(m*qlist/qi) and n modulo n.
*)

Definition allLinCombMod (a : Z) (n m : nat) (qlist : natlist) :=
  alllist nat
    (fun q : nat =>
     LinCombMod 1 (Exp a (m * multDrop q qlist) - 1) (Z_of_nat n) n) qlist.

Lemma allLinCombMod_ok :
 forall (a : Z) (n m : nat) (qlist : natlist),
 allLinCombMod a n m qlist <->
 (forall qi : nat,
  inlist nat qi qlist ->
  LinCombMod 1 (Exp a (m * multDrop qi qlist) - 1) (Z_of_nat n) n).
Proof.
   intros.
   elim
    (alllist_ok nat
       (fun q : nat =>
        LinCombMod 1 (Exp a (m * multDrop q qlist) - 1) (Z_of_nat n) n) qlist).
   split.
   intros. apply H. assumption. assumption.
   intros. apply H0. assumption.
Qed.

(**
   Pocklington's theorem (finally).
   Proves Pocklington for natural numbers.
 *)

Theorem pocklington :
 forall (n q m : nat) (a : Z) (qlist : natlist),
 n > 1 ->
 n = S (q * m) ->
 q = product qlist ->
 allPrime qlist ->
 Mod (Exp a (pred n)) 1 n ->
 allLinCombMod a n m qlist -> n <= q * q -> Prime n.
Proof.
   intros.
   apply primepropdiv. assumption. intro p. intros.
   elim H6. intros. elim H7. intro pdn. intros.
   unfold gt in |- *. apply le_lt_trans with (pred p * pred p).
   apply le_trans with (q * q). assumption.
   cut (q <= pred p). intros.
   apply le_le_mult. assumption. assumption.
   apply order_le_predp with (Exp a m). assumption.
   cut (Mod (Exp (Exp a m) q) 1 p). intros.
   elim (order_ex (Exp a m) p). intro r. intros.
   elim H12. intros. elim H14. intros. elim H16. intros.
   elim (le_lt_or_eq r q). intro.
   cut (Divides r q). intros.
   elim (techlemma3 qlist r q). intro qi. intros.
   elim H21. intros. elim H23. intro rdm. intros.
   elim (allLinCombMod_ok a n m qlist).
   intros AH1 AH2. elim (AH1 H4 qi H22).
   intro alpha. intros. elim H25. intro beta. intros.
   elim (mod_0not1 p). assumption.
   apply mod_trans with ((1 - 1) * alpha + Z_of_nat n * beta)%Z.
   rewrite H10. simpl in |- *.
   rewrite Znat.inj_mult.
   rewrite Zmult_assoc_reverse.
   apply mod_sym.
   apply mod_nx_0_n.
   apply
    mod_trans
     with ((Exp a (m * multDrop qi qlist) - 1) * alpha + Z_of_nat n * beta)%Z.
   apply mod_plus_compat. apply mod_mult_compat. apply mod_minus_compat.
   rewrite H24.
   rewrite mult_assoc.
   apply mod_sym.
   rewrite exp_mult. apply mod_exp1. rewrite exp_mult.
   assumption.
   apply mod_refl. apply mod_refl. apply mod_refl.
   apply mod_sym. apply modpq_modp with pdn. rewrite <- H10. assumption.
   assumption.
   assumption.
   assumption.
   assumption.
   assumption.
   apply (order_div (Exp a m) r p H14 q).
   apply lt_trans with r.
   assumption.
   assumption.
   assumption.
   intro. rewrite <- H19. assumption.
   apply H18.
   elim (le_lt_or_eq 0 q).
   intro. assumption.
   intro. rewrite <- H19 in H5. simpl in H5. elim (le_not_lt n 0). assumption.
   apply lt_trans with 1. apply lt_O_Sn. assumption. apply le_O_n.
   assumption.
   assumption.
   apply mod_not_exp_0.
   assumption.
   intro. elim (mod_0not1 p). assumption.
   apply mod_trans with (Exp a (pred n)).
   apply mod_sym.
   apply moda0_exp_compat.
   unfold gt in |- *. apply lt_trans with 1. apply lt_O_Sn.
   assumption.
   assumption.
   apply gt_pred. assumption.
   rewrite H0. simpl in |- *. rewrite mult_comm. rewrite exp_mult. assumption.
   rewrite H0 in H3. simpl in H3. rewrite <- H0 in H3.
   apply modpq_modp with pdn.
   rewrite <- H10. rewrite <- exp_mult. rewrite mult_comm. assumption.
   apply lt_multpred_pp. assumption.
Qed.

(**
   Below is an attempt to restate Pocklington's theorem
   using only numbers from Z. This will make concrete
   computations faster.
 *)

(** ZallLinCombMod is equivalent to AllLinCombMod but uses Z. *)

Definition ZallLinCombMod (a n m N : Z) (qlist : Zlist) :=
  alllist Z
    (fun q : Z => ZLinCombMod 1 (ZExp a (m * zmultDrop q qlist) - 1) n N)
    qlist.

Lemma ZallLinCombMod_ok :
 forall (a n m N : Z) (qlist : Zlist),
 ZallLinCombMod a n m N qlist ->
 forall qi : Z,
 inlist Z qi qlist -> ZLinCombMod 1 (ZExp a (m * zmultDrop qi qlist) - 1) n N.
Proof.
   intros.
   elim
    (alllist_ok Z
       (fun q : Z => ZLinCombMod 1 (ZExp a (m * zmultDrop q qlist) - 1) n N)
       qlist).
   intros. apply H1. assumption. assumption.
Qed.

Lemma alllincombzalllincomb :
 forall (a n m : Z) (qlist : Zlist),
 (0 <= n)%Z ->
 (0 <= m)%Z ->
 allPos qlist ->
 ZallLinCombMod a n m n qlist ->
 allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map _ _ Z.abs_nat qlist).
Proof.
   intros.
   unfold ZallLinCombMod in H.
   elim
    (alllist_ok Z
       (fun q : Z => ZLinCombMod 1 (ZExp a (m * zmultDrop q qlist) - 1) n n)
       qlist).
   intros.
   elim
    (alllist_ok nat
       (fun q0 : nat =>
        LinCombMod 1
          (Exp a (Z.abs_nat m * multDrop q0 (map _ _ Z.abs_nat qlist)) - 1)
          (Z_of_nat (Z.abs_nat n)) (Z.abs_nat n)) (map _ _ Z.abs_nat qlist)).
   intros.
   apply H6. intros.
   rewrite <- inj_zexp.
   rewrite Znat.inj_mult.
   rewrite inj_abs_pos.
   rewrite inj_abs_pos.
   replace m with (Z_of_nat (Z.abs_nat m)).
   rewrite <- Znat.inj_mult.
   apply zlincombmodlincombmod.
   rewrite Znat.inj_mult. rewrite inj_abs_pos.
   rewrite multdropzmultdrop.
   rewrite inj_abs_pos_list.
   apply H3.
   assumption.
   apply inlist_inj_abs_pos_list.
   assumption. assumption.
   assumption.
   apply Z.le_ge. assumption.
   apply inj_abs_pos.
   apply Z.le_ge. assumption.
   apply Z.le_ge. assumption.
   apply Z.le_ge. assumption.
Qed.

(** Zpocklington is equivalent to pocklington but only uses numbers in Z. *)

Theorem Zpocklington :
 forall (n q m a : Z) (qlist : Zlist),
 (n > 1)%Z ->
 (0 <= q)%Z ->
 (0 <= m)%Z ->
 n = (q * m + 1)%Z ->
 q = zproduct qlist ->
 allZPrime qlist ->
 ZMod (ZExp a (n - 1)) 1 n ->
 ZallLinCombMod a n m n qlist -> (n <= q * q)%Z -> ZPrime n.
Proof.
   intros. cut (0 <= n)%Z. intros.
   rewrite <- (inj_abs_pos n). apply primezprime.
   apply
    (pocklington (Z.abs_nat n) (Z.abs_nat q) (Z.abs_nat m) a
       (map _ _ Z.abs_nat qlist)).
   change (Z.abs_nat n > Z.abs_nat 1) in |- *. apply gtzgt. assumption.
   unfold Z.le in |- *. simpl in |- *. discriminate.
   assumption.
   rewrite H2. rewrite abs_plus_pos. rewrite abs_mult. rewrite plus_comm.
   simpl in |- *. reflexivity.
   apply isnat_mult.
   assumption.
   assumption.
   unfold Z.le in |- *. simpl in |- *. discriminate.
   rewrite H3.
   apply zproductproduct.
   apply allzprimeallprime. assumption.
   apply mod_trans with (ZExp a (n - 1)).
   rewrite <- inj_zexp.
   rewrite abs_pred_pos.
   rewrite inj_abs_pos.
   apply mod_refl.
   apply Z.le_ge.
   unfold Zminus in |- *.
   simpl in |- *.
   change (0 <= 0 + n + -1)%Z in |- *.
   rewrite (Zplus_assoc_reverse 0).
   rewrite Zplus_comm.
   apply (Zlt_left 0 n).
   apply Z.lt_trans with 1%Z.
   unfold Z.lt in |- *.
   simpl in |- *.
   reflexivity.
   apply Z.gt_lt.
   assumption.
   apply Z.lt_trans with 1%Z.
   unfold Z.lt in |- *.
   simpl in |- *.
   reflexivity.
   apply Z.gt_lt.
   assumption.
   apply zmodmod.
   assumption.
   apply alllincombzalllincomb.
   assumption.
   assumption.
   apply allzprimeallpos.
   assumption.
   assumption.
   rewrite <- abs_mult.
   apply lezle.
   assumption.
   apply isnat_mult.
   assumption.
   assumption.
   assumption.
   apply Z.le_ge. assumption.
   apply Z.le_trans with 1%Z.
   unfold Z.le in |- *. simpl in |- *. discriminate.
   apply Zlt_le_weak. apply Z.gt_lt. assumption.
Qed.

author: coq-community

repo: pocklington


text:
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export own.
From iris.base_logic.lib Require Import ghost_map.
From iris.prelude Require Import options.
Import uPred.

Local Notation proph_map P V := (gmap P (list V)).
Definition proph_val_list (P V : Type) := list (P * V).

(** The CMRA we need. *)
Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} := {
  proph_map_preG_inG :> ghost_mapG Σ P (list V)
}.

Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
  proph_map_inG :> proph_mapPreG P V Σ;
  proph_map_name : gname
}.
Global Arguments proph_map_name {_ _ _ _ _} _ : assert.

Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
  #[ghost_mapΣ P (list V)].

Global Instance subG_proph_mapPreG {Σ P V} `{Countable P} :
  subG (proph_mapΣ P V) Σ → proph_mapPreG P V Σ.
Proof. solve_inG. Qed.

Section definitions.
  Context `{pG : proph_mapG P V Σ}.
  Implicit Types pvs : proph_val_list P V.
  Implicit Types R : proph_map P V.
  Implicit Types p : P.

  (** The list of resolves for [p] in [pvs]. *)
  Fixpoint proph_list_resolves pvs p : list V :=
    match pvs with
    | []         => []
    | (q,v)::pvs => if decide (p = q) then v :: proph_list_resolves pvs p
                    else proph_list_resolves pvs p
    end.

  Definition proph_resolves_in_list R pvs :=
    map_Forall (λ p vs, vs = proph_list_resolves pvs p) R.

  Definition proph_map_interp pvs (ps : gset P) : iProp Σ :=
    (∃ R, ⌜proph_resolves_in_list R pvs ∧
          dom (gset _) R ⊆ ps⌝ ∗ ghost_map_auth (proph_map_name pG) 1 R)%I.

  Definition proph_def (p : P) (vs : list V) : iProp Σ :=
    p ↪[proph_map_name pG] vs.

  Definition proph_aux : seal (@proph_def). Proof. by eexists. Qed.
  Definition proph := proph_aux.(unseal).
  Definition proph_eq : @proph = @proph_def := proph_aux.(seal_eq).
End definitions.

Section list_resolves.
  Context {P V : Type} `{Countable P}.
  Implicit Type pvs : proph_val_list P V.
  Implicit Type p : P.
  Implicit Type R : proph_map P V.

  Lemma resolves_insert pvs p R :
    proph_resolves_in_list R pvs →
    p ∉ dom (gset _) R →
    proph_resolves_in_list (<[p := proph_list_resolves pvs p]> R) pvs.
  Proof.
    intros Hinlist Hp q vs HEq.
    destruct (decide (p = q)) as [->|NEq].
    - rewrite lookup_insert in HEq. by inversion HEq.
    - rewrite lookup_insert_ne in HEq; last done. by apply Hinlist.
  Qed.
End list_resolves.

Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
  ⊢ |==> ∃ _ : proph_mapG P V PVS, proph_map_interp pvs ps.
Proof.
  iMod (ghost_map_alloc_empty) as (γ) "Hh".
  iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
  iPureIntro. done.
Qed.

Section proph_map.
  Context `{proph_mapG P V Σ}.
  Implicit Types p : P.
  Implicit Types v : V.
  Implicit Types vs : list V.
  Implicit Types R : proph_map P V.
  Implicit Types ps : gset P.

  (** General properties of mapsto *)
  Global Instance proph_timeless p vs : Timeless (proph p vs).
  Proof. rewrite proph_eq /proph_def. apply _. Qed.

  Lemma proph_exclusive p vs1 vs2 :
    proph p vs1 -∗ proph p vs2 -∗ False.
  Proof.
    rewrite proph_eq /proph_def. iIntros "Hp1 Hp2".
    by iDestruct (ghost_map_elem_ne with "Hp1 Hp2") as %?.
  Qed.

  Lemma proph_map_new_proph p ps pvs :
    p ∉ ps →
    proph_map_interp pvs ps ==∗
    proph_map_interp pvs ({[p]} ∪ ps) ∗ proph p (proph_list_resolves pvs p).
  Proof.
    iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]".
    rewrite proph_eq /proph_def.
    iMod (ghost_map_insert p (proph_list_resolves pvs p) with "H●") as "[H● H◯]".
    { apply (not_elem_of_dom (D:=gset P)). set_solver. }
    iModIntro. iFrame.
    iExists (<[p := proph_list_resolves pvs p]> R).
    iFrame. iPureIntro. split.
    - apply resolves_insert; first done. set_solver.
    - rewrite dom_insert. set_solver.
  Qed.

  Lemma proph_map_resolve_proph p v pvs ps vs :
    proph_map_interp ((p,v) :: pvs) ps ∗ proph p vs ==∗
    ∃vs', ⌜vs = v::vs'⌝ ∗ proph_map_interp pvs ps ∗ proph p vs'.
  Proof.
    iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
    rewrite /proph_map_interp proph_eq /proph_def.
    iDestruct (ghost_map_lookup with "H● Hp") as %HR.
    assert (vs = v :: proph_list_resolves pvs p) as ->.
    { rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
    iMod (ghost_map_update (proph_list_resolves pvs p) with "H● Hp") as "[H● H◯]".
    iModIntro. iExists (proph_list_resolves pvs p). iFrame. iSplitR.
    - iPureIntro. done.
    - iExists _. iFrame. iPureIntro. split.
      + intros q ws HEq. destruct (decide (p = q)) as [<-|NEq].
        * rewrite lookup_insert in HEq. by inversion HEq.
        * rewrite lookup_insert_ne in HEq; last done.
          rewrite (Hres q ws HEq).
          simpl. rewrite decide_False; done.
      + assert (p ∈ dom (gset P) R) by exact: elem_of_dom_2.
        rewrite dom_insert. set_solver.
  Qed.
End proph_map.

author: jtassarotti

repo: iris-inv-hierarchy


text:
Require Import Coq.Program.Program.
Require Export Fiat.Common.Coq__8_4__8_5__Compat.

Set Implicit Arguments.

Notation idmap := (fun x => x).

Class MonadOps (M : Type -> Type)
  := { bind : forall {A B}, M A -> (A -> M B) -> M B;
       ret : forall {A}, A -> M A }.

Global Arguments bind {M _ A B} _ _.
Global Arguments ret {M _ A} _.

Notation "x <- y ; f" := (bind y (fun x => f)) (at level 65, right associativity).

Class MonadLaws M `{MonadOps M}
  := { bind_bind : forall {A B C} (f : A -> M B) (g : B -> M C) x,
                     bind (bind x f) g = bind x (fun u => bind (f u) g);
       bind_unit : forall {A B} (f : A -> M B) x, bind (ret x) f = f x;
       unit_bind : forall {A} (x : M A), bind x ret = x;
       bind_ext : forall {A B} {f g : A -> M B},
                    (forall x, f x = g x)
                    -> forall x, bind x f = bind x g }.

Arguments MonadLaws M {_}.

Class MonadTransformerOps (T : (Type -> Type) -> (Type -> Type))
  := { Tops :> forall M `{MonadOps M}, MonadOps (T M);
       lift : forall {M} `{MonadOps M} {A}, M A -> T M A }.

Class MonadTransformerLaws T `{MonadTransformerOps T}
  := { Tlaws :> forall {M} `{MonadLaws M}, MonadLaws (T M);
       lift_ret : forall {M} `{MonadLaws M} {A} (x : A), lift (ret x) = ret x;
       lift_bind : forall {M} `{MonadLaws M} {A B} (f : A -> M B) x,
                     lift (bind x f) = bind (lift x) (fun u => lift (f u)) }.
Arguments MonadTransformerLaws T {_}.

Create HintDb monad discriminated.
Create HintDb monad' discriminated.
#[global]
Hint Rewrite @bind_bind @bind_unit @unit_bind @lift_ret @lift_bind : monad.
#[global]
Hint Rewrite @bind_unit @unit_bind @lift_ret @lift_bind : monad'.
#[global]
Hint Rewrite <- @bind_bind : monad'.

#[global]
Instance idM : MonadOps idmap
  := { bind A B x f := f x;
       ret A x := x }.
#[global]
Instance idML : MonadLaws idmap.
Proof.
  constructor; trivial.
Defined.

#[global]
Instance idT : MonadTransformerOps idmap
  := { Tops M H := H;
       lift M H A x := x }.
#[global]
Instance idTL : MonadTransformerLaws idmap.
Proof.
  constructor; trivial.
Defined.

#[global]
Instance monad_of_transformer T `{MonadTransformerOps T}
: MonadOps (T idmap) | 1000
  := _.
Coercion monad_of_transformer : MonadTransformerOps >-> MonadOps.

#[global]
Instance monad_laws_of_transformer T `{MonadTransformerLaws T}
: MonadLaws (T idmap)
  := _.
Coercion monad_laws_of_transformer : MonadTransformerLaws >-> MonadLaws.

#[global]
Instance optionT : MonadTransformerOps (fun M => M ∘ option) | 2.
Proof.
  refine {| Tops M H := {| ret A x := ret (Some x);
                        bind A B x f := _ |};
       lift M H A x := bind x (fun a => ret (Some a)) |}.
  { exact (bind (M:=M) x (fun a => match a with
                                   | None => ret None
                                   | Some a' => f a'
                                   end)). }
Defined.

Local Ltac t_option :=
  repeat match goal with
           | _ => intro
           | _ => reflexivity
           | _ => assumption
           | _ => solve [ trivial ]
           | [ H : option _ |- _ ] => destruct H
           | [ |- context[match ?a with None => _ end] ] => case_eq a
           | [ |- @bind ?M ?H ?A ?B ?x _ = bind ?x _ ] => let lem := constr:(@bind_ext M H _ A B) in apply lem
           | [ |- @bind ?M ?H ?A ?B ?x _ = ?x ] => etransitivity; [ | solve [ apply (@unit_bind M H _) ] ]
           | _ => progress autorewrite with monad; try assumption; []
         end.

#[global]
Instance optionTLaws : MonadTransformerLaws (fun M => M ∘ option) | 2.
Proof.
  refine {| Tlaws M H L := _ |}.
  { constructor; simpl; t_option. }
  { simpl; t_option. }
  { simpl; t_option. }
Defined.

#[global]
Instance optionM : MonadOps option | 2 := optionT.
#[global]
Instance optionLaws : MonadLaws option | 2 := optionTLaws.

Definition liftA {T} `{MonadTransformerOps T} {M} `{MonadOps M} {A B}
           (f : M A -> M B)
: T M A -> T M B
  := fun x => y <- x; lift (f (ret y)).

author: mit-plv

repo: fiat

save_path: github-repos/coq/mit-plv-fiat


Require Import msl.log_normalize.
Require Import msl.alg_seplog.
Require Export veric.base.
Require Import veric.compcert_rmaps.
Require Import veric.slice.
Require Import veric.tycontext.
Require Import veric.expr2.
Require Import veric.binop_lemmas2.

Local Open Scope pred.

Definition tc_expr {CS: compspecs}  (Delta: tycontext) (e: expr) : environ -> mpred:=
  fun rho => denote_tc_assert (typecheck_expr Delta e) rho.

Definition tc_exprlist {CS: compspecs} (Delta: tycontext) (t : list type) (e: list expr) : environ -> mpred :=
      fun rho => denote_tc_assert (typecheck_exprlist Delta t e) rho.

Definition tc_lvalue {CS: compspecs} (Delta: tycontext) (e: expr) : environ -> mpred :=
     fun rho => denote_tc_assert (typecheck_lvalue Delta e) rho.

Definition allowedValCast v tfrom tto :=
match Cop.classify_cast tfrom tto with
| Cop.cast_case_neutral => if andb (is_int_type tfrom) (is_pointer_type tto)
                          then
                            match v with
                              | Vint i => (Int.eq i Int.zero)
                              | _ => false
                            end
                          else if eqb (is_int_type tfrom)
                                      (is_int_type tto)
                               then true else false
| Cop.cast_case_i2i _ _ => true
| Cop.cast_case_l2l => true
| Cop.cast_case_f2f => true
| Cop.cast_case_s2s => true
| _  => false
end.

Definition tc_temp_id {CS: compspecs} (id : positive) (ty : type)
  (Delta : tycontext) (e : expr) : environ -> mpred  :=
     fun rho => denote_tc_assert (typecheck_temp_id id ty Delta e) rho.

Definition tc_temp_id_load id tfrom Delta v : environ -> mpred  :=
fun rho => !! (exists tto, exists x, (temp_types Delta) ! id = Some (tto, x)
                      /\ tc_val tto (eval_cast tfrom tto (v rho))).

Lemma extend_prop: forall P, boxy extendM (prop P).
Proof.
intros.
hnf.
apply pred_ext. intros ? ?. apply H; auto. apply extendM_refl.
repeat intro. apply H.
Qed.

Hint Resolve extend_prop.

Lemma extend_tc_temp_id_load :  forall id tfrom Delta v rho, boxy extendM (tc_temp_id_load id tfrom Delta v rho).
Proof.
intros. unfold tc_temp_id_load. auto.
Qed.

Lemma extend_tc_andp:
 forall {CS: compspecs} A B rho,
   boxy extendM (denote_tc_assert A rho) ->
   boxy extendM (denote_tc_assert B rho) ->
   boxy extendM (denote_tc_assert (tc_andp A B) rho).
Proof.
intros.
rewrite denote_tc_assert_andp.
apply boxy_andp; auto.
apply extendM_refl.
Qed.

Lemma extend_tc_bool:
 forall {CS: compspecs} A B rho,
   boxy extendM (denote_tc_assert (tc_bool A B) rho).
Proof.
intros.
destruct A; simpl; apply  extend_prop.
Qed.

Lemma extend_tc_Zge:
 forall {CS: compspecs} v i rho,
   boxy extendM (denote_tc_assert (tc_Zge v i) rho).
Proof.
intros.
induction v; simpl; unfold_lift; simpl;
unfold denote_tc_Zle; try apply extend_prop;
repeat match goal with |- boxy _ (match ?A with  _ => _ end) => destruct A end;
try apply extend_prop.
Qed.

Lemma extend_tc_Zle:
 forall {CS: compspecs} v i rho,
   boxy extendM (denote_tc_assert (tc_Zle v i) rho).
Proof.
intros.
induction v; simpl; unfold_lift; simpl;
unfold denote_tc_Zge; try apply extend_prop;
repeat match goal with |- boxy _ (match ?A with  _ => _ end) => destruct A end;
try apply extend_prop.
Qed.

Lemma extend_tc_iszero:
 forall {CS: compspecs} v rho,
   boxy extendM (denote_tc_assert (tc_iszero v) rho).
Proof.
intros.
rewrite denote_tc_assert_iszero.
destruct (eval_expr v rho); apply extend_prop.
Qed.

Lemma extend_valid_pointer':
  forall a b, boxy extendM (valid_pointer' a b).
Proof.
intros.
apply boxy_i; intros.
apply extendM_refl.
unfold valid_pointer' in *.
simpl in *.
destruct a; simpl in *; auto.
forget (b0, Int.unsigned i + b) as p.
destruct (w @ p) eqn:?H; try contradiction.
destruct H as [w2 ?].
apply (resource_at_join _ _ _ p) in H.
rewrite H1 in H.
inv H; auto.
clear - H0 RJ.
eapply join_nonidentity; eauto.
destruct H as [w2 ?].
apply (resource_at_join _ _ _ p) in H.
rewrite H1 in H.
inv H; auto.
Qed.

Lemma extend_tc_test_eq:
  forall {CS: compspecs} e1 e2 rho,
 boxy extendM (denote_tc_assert (tc_test_eq e1 e2) rho).
Proof.
intros.
rewrite denote_tc_assert_test_eq'.
apply boxy_i; intros.
apply extendM_refl.
simpl in *.
super_unfold_lift.
unfold denote_tc_test_eq in *.
destruct (eval_expr e1 rho); auto;
destruct (eval_expr e2 rho); auto.
+ destruct H0; split; auto.
  destruct H1 as [H1|H1]; [left|right];
  apply (boxy_e _ _ (extend_valid_pointer' _ _) _ w' H H1).
+ destruct H0; split; auto.
  destruct H1 as [H1|H1]; [left|right];
  apply (boxy_e _ _ (extend_valid_pointer' _ _) _ w' H H1).
+ destruct H0; split; auto.
  destruct H1 as [H1|H1]; [left|right];
  apply (boxy_e _ _ (extend_valid_pointer' _ _) _ w' H H1).
+ destruct H0; split; auto.
  destruct H1 as [H1|H1]; [left|right];
  apply (boxy_e _ _ (extend_valid_pointer' _ _) _ w' H H1).
+ unfold test_eq_ptrs in *.
  simpl cast_out_long in H0 |- *.
  cbv iota beta in H0 |- *.
  if_tac.
  - destruct H0; split.
    * destruct H0 as [?|?]; [left|right];
      apply (boxy_e _ _ (extend_valid_pointer' _ _) _ w' H H0).
    * destruct H1 as [?|?]; [left|right];
      apply (boxy_e _ _ (extend_valid_pointer' _ _) _ w' H H1).
  - destruct H0; split.
    * apply (boxy_e _ _ (extend_valid_pointer' _ _) _ w' H H0).
    * apply (boxy_e _ _ (extend_valid_pointer' _ _) _ w' H H1).
Qed.

Lemma extend_tc_test_order:
  forall {CS: compspecs} e1 e2 rho,
 boxy extendM (denote_tc_assert (tc_test_order e1 e2) rho).
Proof.
intros.
rewrite denote_tc_assert_test_order'.
apply boxy_i; intros.
apply extendM_refl.
simpl in *.
super_unfold_lift.
unfold denote_tc_test_order in *.
destruct (eval_expr e1 rho); auto;
destruct (eval_expr e2 rho); auto.
+ unfold test_order_ptrs in *.
  simpl cast_out_long in H0 |- *.
  cbv iota beta in H0 |- *.
  if_tac.
  - destruct H0; split.
    * destruct H0 as [?|?]; [left|right];
      apply (boxy_e _ _ (extend_valid_pointer' _ _) _ w' H H0).
    * destruct H1 as [?|?]; [left|right];
      apply (boxy_e _ _ (extend_valid_pointer' _ _) _ w' H H1).
  - auto.
Qed.

Lemma extend_isCastResultType:
 forall {CS: compspecs} t t' v rho,
   boxy extendM (denote_tc_assert (isCastResultType t t' v) rho).
Proof.
intros.
 unfold isCastResultType;
 destruct (Cop.classify_cast t t');
 repeat apply extend_tc_andp;
 try match goal with |- context [eqb_type _ _] => destruct (eqb_type t t') end;
 repeat match goal with
 | |- boxy _ (match ?A with  _ => _ end) => destruct A
 | |- boxy _ (denote_tc_assert (if ?A then _ else _) rho) => destruct A
 | |- boxy _ (denote_tc_assert (match t' with _ => _ end) rho) =>
        destruct t' as [ | [ | | | ] [ | ] ? | [ | ] ? | [ | ] ? | | | | | ]
 end;
 repeat apply extend_tc_andp;
 try apply extend_prop;
 try simple apply extend_tc_bool;
 try simple apply extend_tc_Zge;
 try simple apply extend_tc_Zle;
 try simple apply extend_tc_iszero;
 try simple apply extend_tc_test_eq;
 try simple apply extend_tc_test_order.
Qed.

Lemma extend_tc_temp_id: forall {CS: compspecs} id ty Delta e rho, boxy extendM (tc_temp_id id ty Delta e rho).
Proof.
intros. unfold tc_temp_id. unfold typecheck_temp_id.
destruct ((temp_types Delta) ! id) as [[? ?] | ];
 repeat apply extend_tc_andp;
 try apply extend_prop;
 try simple apply extend_tc_bool.
 apply extend_isCastResultType.
Qed.

Lemma extend_tc_samebase:
  forall {CS: compspecs} e1 e2 rho,
boxy extendM (denote_tc_assert (tc_samebase e1 e2) rho).
Proof.
intros.
unfold denote_tc_assert; simpl.
unfold_lift.
destruct (eval_expr e1 rho), (eval_expr e2 rho);
  apply extend_prop.
Qed.

Lemma extend_tc_nonzero:
 forall {CS: compspecs} v rho,
   boxy extendM (denote_tc_assert (tc_nonzero v) rho).
Proof.
intros.
rewrite denote_tc_assert_nonzero.
destruct (eval_expr v rho); apply extend_prop.
Qed.

Lemma extend_tc_nodivover:
 forall {CS: compspecs} e1 e2 rho,
   boxy extendM (denote_tc_assert (tc_nodivover e1 e2) rho).
Proof.
intros.
rewrite denote_tc_assert_nodivover.
destruct (eval_expr e1 rho); try apply extend_prop;
destruct (eval_expr e2 rho); try apply extend_prop.
Qed.

Lemma boxy_orp {A} `{H : ageable A}:
     forall (M: modality) , reflexive _ (app_mode M) ->
      forall P Q, boxy M P -> boxy M Q -> boxy M (P || Q).
Proof.
destruct M;
intros.
simpl in *.
apply boxy_i; intros; auto.
destruct H4; [left|right];
eapply boxy_e; eauto.
Qed.

Lemma extend_tc_orp:
 forall {CS: compspecs} A B rho,
   boxy extendM (denote_tc_assert A rho) ->
   boxy extendM (denote_tc_assert B rho) ->
   boxy extendM (denote_tc_assert (tc_orp A B) rho).
Proof.
intros.
rewrite denote_tc_assert_orp.
apply boxy_orp; auto.
apply extendM_refl.
Qed.

Lemma extend_tc_ilt:
 forall {CS: compspecs} e i rho,
   boxy extendM (denote_tc_assert (tc_ilt e i) rho).
Proof.
intros.
rewrite denote_tc_assert_ilt'.
simpl. unfold_lift.
destruct (eval_expr e rho); try apply extend_prop.
Qed.

Lemma extend_tc_expr: forall {CS: compspecs} Delta e rho, boxy extendM (tc_expr Delta e rho)
 with extend_tc_lvalue: forall {CS: compspecs} Delta e rho, boxy extendM (tc_lvalue Delta e rho).
Proof.
*
 clear extend_tc_expr.
 intros.
unfold tc_expr.
  induction e; simpl;
  destruct t as [ | [ | | | ] [ | ] ? | [ | ] ? | [ | ] ? | | | | | ];
  simpl;
 unfold isBinOpResultType, binarithType;
 try (destruct u; simpl);
 repeat apply extend_tc_andp;
 repeat match goal with
 | |- boxy _ (denote_tc_assert match ?A with  _ => _ end _) => destruct A
 | |- boxy _ (denote_tc_assert (if ?A then _ else _) rho) => destruct A
 | |- context [typeof ?e] =>
      destruct (typeof e) as [ | [ | | | ] [ | ] ? | [ | ] ? | [ | ] ? | | | | | ];
      try apply extend_prop
 end;
 repeat apply extend_tc_andp;
 repeat apply extend_tc_orp;
 repeat apply extend_tc_andp;
 try apply extend_prop;
 try simple apply extend_tc_bool;
 try simple apply extend_tc_Zge;
 try simple apply extend_tc_Zle;
 try simple apply extend_tc_iszero;
 try simple apply extend_tc_nonzero;
 try simple apply extend_tc_nodivover;
 try simple apply extend_tc_samebase;
 try simple apply extend_tc_ilt;
 try simple apply extend_isCastResultType;
 try simple apply extend_tc_test_eq;
 try simple apply extend_tc_test_order;
 auto;
 try apply extend_tc_lvalue.
*
 clear extend_tc_lvalue.
 intros.
 unfold tc_lvalue.
 induction e; simpl;
 try apply extend_prop;
 repeat apply extend_tc_andp;
 repeat match goal with
 | |- boxy _ (denote_tc_assert match ?A with  _ => _ end _) => destruct A
 | |- boxy _ (denote_tc_assert (if ?A then _ else _) rho) => destruct A
 | |- context [typeof ?e] =>
      destruct (typeof e) as [ | [ | | | ] [ | ] ? | [ | ] ? | [ | ] ? | | | | | ];
      try apply extend_prop
 end;
 repeat apply extend_tc_andp;
 repeat apply extend_tc_orp;
 repeat apply extend_tc_andp;
 try apply extend_prop;
 try simple apply extend_tc_bool;
 try simple apply extend_tc_Zge;
 try simple apply extend_tc_Zle;
 try simple apply extend_tc_iszero;
 try simple apply extend_tc_nonzero;
 try simple apply extend_tc_nodivover;
 try simple apply extend_tc_samebase;
 try simple apply extend_tc_ilt;
 try simple apply extend_isCastResultType;
 try simple apply extend_tc_test_eq;
 try simple apply extend_tc_test_order;
 auto;
 try apply extend_tc_lvalue.
 apply extend_tc_expr.
Qed.

Lemma extend_tc_exprlist: forall {CS: compspecs} Delta t e rho, boxy extendM (tc_exprlist Delta t e rho).
Proof.
 intros. unfold tc_exprlist.
  revert e; induction t; destruct e; intros; simpl; auto;
  try apply extend_prop.
 repeat apply extend_tc_andp; auto.
 apply extend_tc_expr.
 try simple apply extend_isCastResultType.
Qed.

Hint Resolve extend_tc_expr extend_tc_temp_id extend_tc_temp_id_load extend_tc_exprlist extend_tc_lvalue.
Hint Resolve (@extendM_refl rmap _ _ _ _ _).


text:
Require Export Arith.

Definition task :=
  forall m n, S m < n -> m < (m + n) / 2 < n.

author: tzik

repo: top-prover

save_path: github-repos/coq/tzik-top-prover


text:
(* Proof that Q is a countable setoid *)

Require Import Lia SetoidClass BinPos Recdef Util Arith.

Record Qpos := mkQp { Qnump : positive; Qdenp : positive }.

Instance Qpos_Setoid : Setoid Qpos :=
  {|
    equiv := fun p q => (Qnump p * Qdenp q = Qnump q * Qdenp p)%positive
  |}.
Proof.
  split.
  - intros []; simpl.
    lia.
  - intros [] []; simpl.
    lia.
  - intros [a b] [c d] [e f]; simpl.
    intros.
    apply (Pos.mul_cancel_l _ _ d).
    rewrite (Pos.mul_assoc d a f).
    rewrite (Pos.mul_comm d a).
    rewrite H.
    rewrite <- (Pos.mul_assoc c b f).
    rewrite (Pos.mul_comm b f).
    rewrite (Pos.mul_assoc c f b).
    rewrite H0; lia.
Defined.

Inductive BinPath :=
  | Empty : BinPath
  | Left : BinPath -> BinPath
  | Right : BinPath -> BinPath.

Definition qp_left : Qpos -> Qpos :=
  fun q => match q with
           | mkQp a b => mkQp a (a + b)
           end.

Definition qp_right : Qpos -> Qpos :=
  fun q => match q with
           | mkQp a b => mkQp (a + b) b
           end.

Lemma qp_left_morph : forall q q', q == q' -> qp_left q == qp_left q'.
Proof.
  intros [] [] G.
  simpl in G.
  unfold qp_left; simpl.
  lia.
Qed.

Lemma qp_right_morph : forall q q', q == q' -> qp_right q == qp_right q'.
Proof.
  intros [] [] G.
  simpl in G.
  unfold qp_right; simpl.
  lia.
Qed.

Fixpoint BinPath_to_Qpos(x : BinPath) : Qpos :=
  match x with
  | Empty => mkQp 1 1
  | Left p => qp_left (BinPath_to_Qpos p)
  | Right p => qp_right (BinPath_to_Qpos p)
  end.

Lemma pos_trich : forall x y : positive,
  {(x < y)%positive} + {(y < x)%positive} + {x = y}.
Proof.
  induction x; destruct y;
  try destruct (IHx y) as [[|]|].
  - left; left; lia.
  - left; right; lia.
  - right; lia.
  - left; left; lia.
  - left; right; lia.
  - left; right; lia.
  - left; right; lia.
  - left; left; lia.
  - left; right; lia.
  - left; left; lia.
  - left; left; lia.
  - left; right; lia.
  - right; lia.
  - left; right; lia.
  - left; left; lia.
  - left; left; lia.
  - right; lia.
Defined.

Lemma pos_trich2 : forall x y : positive,
  {_ : unit & x = y} + {z : positive & (x + z = y)%positive} + {z : positive & (y + z = x)%positive}.
Proof.
  intros.
  destruct (pos_trich x y) as [[|]|].
  - left; right; exists (y-x)%positive; lia.
  - right; exists (x-y)%positive; lia.
  - left; left; exists tt; auto.
Defined.

Lemma pos_trich2_inl_inl : forall x y p, x == y ->
  pos_trich2 (Qnump x) (Qdenp x) = inl (inl p) -> exists q, pos_trich2 (Qnump y) (Qdenp y) = inl (inl q).
Proof.
  intros.
  simpl in H.
  destruct (pos_trich2 (Qnump y) (Qdenp y)) as [[|]|].
  - exists s; reflexivity.
  - destruct s as [z Hz].
    clear H0.
    destruct p as [_ G].
    rewrite <- Hz in H.
    rewrite G in H.
    rewrite Pos.mul_add_distr_l in H.
    rewrite (Pos.mul_comm (Qdenp x)) in H.
    absurd (Qnump y * Qdenp x < Qnump y * Qdenp x)%positive.
    + lia.
    + rewrite <- H at 2.
      apply Pos.lt_add_diag_r.
  - destruct s as [z Hz].
    clear H0.
    destruct p as [_ G].
    rewrite G in H.
    rewrite <- Hz in H.
    rewrite Pos.mul_add_distr_r in H.
    rewrite (Pos.mul_comm (Qdenp x)) in H.
    absurd (Qdenp y * Qdenp x < Qdenp y * Qdenp x)%positive.
    + lia.
    + rewrite H at 2.
      apply Pos.lt_add_diag_r.
Qed.

Lemma pos_trich2_inl_inr : forall x y p, x == y ->
  pos_trich2 (Qnump x) (Qdenp x) = inl (inr p) -> exists q, pos_trich2 (Qnump y) (Qdenp y) = inl (inr q).
Proof.
  intros.
  simpl in H.
  destruct p.
  clear H0.
  destruct (pos_trich2 (Qnump y) (Qdenp y)) as [[|]|].
  - destruct s.
    rewrite e0 in H.
    rewrite <- e in H.
    rewrite Pos.mul_add_distr_l in H.
    absurd (Qnump x * Qdenp y < Qnump x * Qdenp y)%positive.
    + lia.
    + rewrite H at 2.
      rewrite (Pos.mul_comm (Qdenp y)).
      apply Pos.lt_add_diag_r.
  - exists s; auto.
  - destruct s.
    rewrite <- e0 in H.
    rewrite <- e in H.
    rewrite Pos.mul_add_distr_r in H.
    absurd (Qnump x * Qdenp y < Qnump x * Qdenp y)%positive.
    + lia.
    + rewrite H at 2.
      rewrite (Pos.mul_comm (Qdenp y)).
      rewrite Pos.mul_add_distr_r.
      rewrite <- Pos.add_assoc.
      apply Pos.lt_add_diag_r.
Qed.

Lemma pos_trich2_inr : forall x y p, x == y ->
  pos_trich2 (Qnump x) (Qdenp x) = (inr p) -> exists q, pos_trich2 (Qnump y) (Qdenp y) = (inr q).
Proof.
  intros.
  simpl in H.
  destruct p.
  clear H0.
  destruct (pos_trich2 (Qnump y) (Qdenp y)) as [[|]|].
  - destruct s.
    rewrite e0 in H.
    rewrite <- e in H.
    rewrite Pos.mul_add_distr_r in H.
    absurd (Qdenp x * Qdenp y < Qdenp x * Qdenp y)%positive.
    + lia.
    + rewrite (Pos.mul_comm (Qdenp y)) in H.
      rewrite <- H at 2.
      apply Pos.lt_add_diag_r.
  - destruct s.
    rewrite <- e0 in H.
    rewrite <- e in H.
    rewrite Pos.mul_add_distr_r in H.
    absurd (Qdenp x * Qnump y < Qdenp x * Qnump y)%positive.
    + lia.
    + rewrite (Pos.mul_comm (Qnump y)) in H.
      rewrite <- H at 2.
      rewrite Pos.mul_add_distr_l.
      rewrite <- Pos.add_assoc.
      apply Pos.lt_add_diag_r.
  - exists s; auto.
Qed.

Function Qpos_to_BinPath(q : Qpos){measure (fun x => Pos.to_nat (Qnump x + Qdenp x))%positive} : BinPath :=
  match pos_trich2 (Qnump q) (Qdenp q) with
  | inl (inl _) => Empty
  | inl (inr (existT _ z _)) => Left (Qpos_to_BinPath (mkQp (Qnump q) z))
  | inr (existT _ z _) => Right (Qpos_to_BinPath (mkQp z (Qdenp q)))
  end.
Proof.
  - intros.
    apply Pnat.Pos2Nat.inj_lt.
    simpl.
    rewrite e.
    rewrite Pos.add_comm.
    apply Pos.lt_add_diag_r.
  - intros.
    apply Pnat.Pos2Nat.inj_lt.
    simpl.
    rewrite (Pos.add_comm z).
    rewrite e.
    apply Pos.lt_add_diag_r.
Defined.

Lemma Qpos_to_BinPath_morph : forall q q', q == q' ->
  Qpos_to_BinPath q = Qpos_to_BinPath q'.
Proof.
  intro q; apply Qpos_to_BinPath_ind; intros;
  rewrite Qpos_to_BinPath_equation.
  - destruct (pos_trich2_inl_inl _ _ _ H e).
    rewrite H0; auto.
  - rewrite (Qpos_to_BinPath_equation q').
    destruct (pos_trich2_inl_inr _ _ _  H0 e).
    rewrite H1.
    destruct x.
    rewrite <- H.
    + f_equal.
      simpl.
      rewrite Qpos_to_BinPath_equation.
      simpl.
      reflexivity.
    + simpl in H0.
      rewrite <- _x in H0.
      rewrite <- e0 in H0.
      simpl.
      lia.
  - rewrite (Qpos_to_BinPath_equation q').
    destruct (pos_trich2_inr _ _ _ H0 e).
    rewrite H1.
    destruct x.
    rewrite <- H.
    + f_equal.
      simpl.
      rewrite Qpos_to_BinPath_equation.
      simpl.
      reflexivity.
    + simpl in H0.
      rewrite <- e0 in H0.
      rewrite <- _x in H0.
      simpl.
      lia.
Qed.

Lemma Qpos_to_from : forall q, BinPath_to_Qpos (Qpos_to_BinPath q) == q.
Proof.
  intro.
  apply Qpos_to_BinPath_ind.
  - intros.
    simpl.
    destruct _x.
    rewrite e0.
    lia.
 - intros.
    simpl.
    pose ((BinPath_to_Qpos
      (Qpos_to_BinPath {| Qnump := Qnump q0; Qdenp := z |}))) as x.
    fold x.
    fold x in H.
    unfold qp_left.
    destruct x.
    simpl.
    simpl in H.
    rewrite <- _x.
    rewrite Pos.mul_add_distr_l.
    rewrite H.
    lia.
  - intros.
    simpl.
    pose (BinPath_to_Qpos (Qpos_to_BinPath {| Qnump := z; Qdenp := Qdenp q0 |})) as x.
    fold x.
    fold x in H.
    unfold qp_right.
    destruct x.
    simpl.
    simpl in H.
    rewrite <- _x.
    rewrite Pos.mul_add_distr_r.
    rewrite H.
    lia.
Qed.

Lemma qp_left_Left : forall x, Qpos_to_BinPath (qp_left x) = Left
  (Qpos_to_BinPath x).
Proof.
  intros.
  unfold qp_left.
  destruct x.
  rewrite Qpos_to_BinPath_equation.
  simpl.
  destruct pos_trich2 as [[|]|].
  - destruct s.
    lia.
  - destruct s.
    assert (x = Qdenp0) by lia.
    rewrite H.
    auto.
  - destruct s.
    lia.
Qed.

Lemma qp_right_Right : forall x, Qpos_to_BinPath (qp_right x) = Right
  (Qpos_to_BinPath x).
Proof.
  intros.
  unfold qp_right.
  destruct x.
  rewrite Qpos_to_BinPath_equation.
  simpl.
  destruct pos_trich2 as [[|]|].
  - destruct s.
    lia.
  - destruct s.
    lia.
  - destruct s.
    assert (x = Qnump0) by lia.
    rewrite H.
    auto.
Qed.

Lemma Qpos_from_to : forall x, Qpos_to_BinPath (BinPath_to_Qpos x) = x.
Proof.
  intro.
  induction x.
  - simpl.
    rewrite Qpos_to_BinPath_equation.
    destruct pos_trich2 as [[|]|].
    + reflexivity.
    + destruct s as [z Hz].
      simpl Qnump in Hz; simpl Qdenp in Hz; lia.
    + destruct s as [z Hz].
      simpl Qnump in Hz; simpl Qdenp in Hz; lia.
  - simpl.
    rewrite qp_left_Left.
    rewrite IHx; auto.
  - simpl.
    rewrite qp_right_Right.
    rewrite IHx; auto.
Qed.

Fixpoint path_to_nat(x : BinPath) : nat :=
  match x with
  | Empty => 0
  | Left y => S (2 * path_to_nat y)
  | Right y => S (S (2 * path_to_nat y))
  end.

Lemma path_to_nat_Left : forall x,
  path_to_nat (Left x) = S (2 * path_to_nat x).
Proof.
  auto.
Qed.

Lemma path_to_nat_Right : forall x,
  path_to_nat (Right x) = S (S (2 * path_to_nat x)).
Proof.
  auto.
Qed.

Function path_from_nat(n : nat){measure id n} : BinPath :=
  match n with
  | 0 => Empty
  | S m => if Util.even m then Left (path_from_nat (m/2)) else Right (path_from_nat (m/2))
  end.
Proof.
  - intros; unfold id.
    destruct (even_half _ teq0) as [k Hk].
    rewrite <- Hk.
    rewrite half_2k.
    lia.
  - intros.
    unfold id.
    destruct (odd_half _ teq0) as [k Hk].
    rewrite <- Hk.
    rewrite half_2k1.
    lia.
Defined.

Lemma path_from_to : forall x, path_from_nat (path_to_nat x) = x.
Proof.
  induction x.
  - auto.
  - rewrite path_to_nat_Left.
    rewrite path_from_nat_equation.
    rewrite even_2k.
    rewrite half_2k.
    rewrite IHx; auto.
  - rewrite path_to_nat_Right.
    rewrite path_from_nat_equation.
    rewrite odd_2k1.
    rewrite half_2k1.
    rewrite IHx; auto.
Qed.

Lemma path_to_from : forall x, path_to_nat (path_from_nat x) = x.
Proof.
  intro x.
  apply path_from_nat_ind.
  - auto.
  - intros.
    rewrite path_to_nat_Left.
    rewrite H.
    destruct (even_half _ e0) as [k Hk].
    rewrite <- Hk.
    rewrite half_2k; auto.
  - intros.
    rewrite path_to_nat_Right.
    rewrite H.
    destruct (odd_half _ e0) as [k Hk].
    rewrite <- Hk.
    rewrite half_2k1; auto.
Qed.

Definition Qpos_to_nat : Qpos -> nat :=
  fun q => path_to_nat (Qpos_to_BinPath q).

Definition nat_to_Qpos : nat -> Qpos :=
  fun x => BinPath_to_Qpos (path_from_nat x).

Lemma Qpos_to_nat_morph : forall q q',
  q == q' -> Qpos_to_nat q = Qpos_to_nat q'.
Proof.
  intros.
  unfold Qpos_to_nat.
  f_equal.
  apply Qpos_to_BinPath_morph; auto.
Qed.

Lemma Qpos_nat_to_from : forall x, Qpos_to_nat (nat_to_Qpos x) = x.
Proof.
  intro.
  unfold Qpos_to_nat.
  unfold nat_to_Qpos.
  rewrite Qpos_from_to.
  apply path_to_from.
Qed.

Lemma Qpos_nat_from_to : forall x, nat_to_Qpos (Qpos_to_nat x) == x.
Proof.
  intro.
  unfold nat_to_Qpos.
  unfold Qpos_to_nat.
  rewrite path_from_to.
  apply Qpos_to_from.
Qed.

Require Import QArith SetoidClass.

Definition Qpos_to_Q_pos : Qpos -> Q :=
  fun q => match q with
           | mkQp a b => Qmake (Zpos a) b
           end.

Definition Qpos_to_Q_neg : Qpos -> Q :=
  fun q => match q with
           | mkQp a b => Qmake (Zneg a) b
           end.

Definition Q_to_nat : Q -> nat :=
  fun q => match q with
           | Qmake Z0 _ => 0%nat
           | Qmake (Zpos p) d => S (2 * Qpos_to_nat (mkQp p d))
           | Qmake (Zneg p) d => S (S (2 * Qpos_to_nat (mkQp p d)))
           end.

Definition nat_to_Q : nat -> Q :=
  fun n => match n with
           | 0%nat => 0
           | S m => if even m then (Qpos_to_Q_pos (nat_to_Qpos (m/2)))
                      else (Qpos_to_Q_neg (nat_to_Qpos (m/2)))
           end.

Instance Setoid_Q : Setoid Q := {|
  equiv := Qeq
  |}.

Lemma Q_to_nat_morph : forall q q', q == q' -> Q_to_nat q = Q_to_nat q'.
Proof.
  intros.
  simpl in H.
  unfold Q_to_nat.
  destruct q,q'.
  unfold Qeq in H.
  destruct Qnum, Qnum0; try auto; try discriminate.
  - simpl in H.
    f_equal.
    f_equal.
    unfold Qpos_to_nat.
    f_equal.
    apply Qpos_to_BinPath_morph.
    simpl.
    inversion H; auto.
  - simpl in H.
    f_equal; f_equal; f_equal.
    unfold Qpos_to_nat; f_equal.
    apply Qpos_to_BinPath_morph.
    simpl.
    inversion H; auto.
Qed.

Lemma Q_to_from : forall x, Q_to_nat (nat_to_Q x) = x.
Proof.
  intro.
  unfold Q_to_nat.
  unfold nat_to_Q.
  destruct x.
  - reflexivity.
  - destruct (even x) eqn:G.
    + unfold Qpos_to_Q_pos.
      destruct nat_to_Qpos eqn:G1.
      rewrite <- G1.
      rewrite Qpos_nat_to_from.
      destruct (even_half _ G) as [k Hk].
      rewrite <- Hk.
      rewrite half_2k; auto.
    + unfold Qpos_to_Q_neg.
      destruct nat_to_Qpos eqn:G2.
      rewrite <- G2.
      rewrite Qpos_nat_to_from.
      destruct (odd_half _ G) as [k Hk].
      rewrite <- Hk.
      rewrite half_2k1; auto.
Qed.

Lemma Q_from_to : forall x, nat_to_Q (Q_to_nat x) == x.
Proof.
  intro.
  unfold Q_to_nat.
  unfold nat_to_Q.
  destruct x.
  destruct Qnum.
  - simpl; unfold Qeq.
    simpl; lia.
  - rewrite even_2k.
    unfold Qpos_to_Q_pos.
    rewrite half_2k.
    destruct nat_to_Qpos eqn:G.
    pose (Qpos_nat_from_to {| Qnump := p; Qdenp := Qden |}).
    rewrite G in e.
    simpl in e.
    simpl.
    unfold Qeq.
    simpl.
    f_equal.
    auto.
  - rewrite odd_2k1.
    unfold Qpos_to_Q_neg.
    rewrite half_2k1.
    destruct nat_to_Qpos eqn:G.
    pose (Qpos_nat_from_to {| Qnump := p; Qdenp := Qden |}).
    rewrite G in e.
    simpl in e.
    simpl.
    unfold Qeq.
    simpl.
    f_equal.
    auto.
Qed.

author: emarzion

repo: cantor

save_path: github-repos/coq/emarzion-cantor


text:
(** Cheat sheet available at
      #https://www-sop.inria.fr/teams/marelle/types18/cheatsheet.pdf#
*)

From mathcomp Require Import all_ssreflect.

Implicit Type p q r : bool.
Implicit Type m n a b c : nat.

(**
-----------------------------------------------------------------
#
#
*** Exercise 1:
    - prove this satement by induction
#
#
*)
Lemma iterSr A n (f : A -> A) x : iter n.+1 f x = iter n f (f x).
(*A*)Proof. by elim: n => //= n <-. Qed.

(**
#
#

#

#
#
#

----------------------------------------------------------
#
#

*** Exercise 2:
    - look up the definition of [iter] (note there is an accumulator varying
      during recursion)
    - prove the following statement by induction

#
#
*)
Lemma iter_predn m n : iter n predn m = m - n.
Proof.
(*D*)by elim: n m => [|n IHn] m; rewrite ?subn0//= IHn subnS.
(*A*)Qed.
(**
#
#

#

#
#
#

----------------------------------------------------------
#
#

*** Exercise 3:

Prove the sum of the lists [odds n] of exercise 1 is [n ^ 2].

You can prove the following lemmas in any order, some are way easier
than others.

- Recall from exercise 1.
#
#

*)
Definition add2list s := map (fun x => x.+2) s.
Definition odds n := iter n (fun s => 1 :: add2list s) [::].
(**
#
#

- We define a sum operation [suml].

#
#

*)
Definition suml := foldl addn 0.
(**
#
#

- Any [foldl addn] can be rexpressed as a sum.

#
#
*)
Lemma foldl_addE n s : foldl addn n s = n + suml s.
Proof.
(*D*)elim: s n => //= x s IHs n.
(*D*)by rewrite /suml/= !IHs add0n addnA.
(*A*)Qed.
(**
#
#

- Not to break abstraction, prove [suml_cons].
#
#
*)
Lemma suml_cons n s : suml (n :: s) = n + suml s.
(*A*)Proof. by rewrite /suml/= foldl_addE. Qed.
(**
#
#

- Show how to sum a [add2list].

#
#
*)
Lemma suml_add2list s : suml (add2list s) = suml s + 2 * size s.
Proof.
(*D*)elim: s => [|x s IHs] //=; rewrite !suml_cons IHs.
(*D*)by rewrite !mulnS !addnS addnA.
(*A*)Qed.
(**
#
#

- Show the size of a [add2list].

#
#
*)
Lemma size_add2list s : size (add2list s) = size s.
(*A*)Proof. by apply: size_map. Qed.
(**
#
#

- Show how many elments [odds] have.

#
#
*)
Lemma size_odds n : size (odds n) = n.
(*A*)Proof. by elim: n => //= n; rewrite size_add2list => ->. Qed.
(**
#
#
- Show the final statment.
#
#
*)
Lemma eq_suml_odds n : suml (odds n) = n ^ 2.
Proof.
(*D*)elim: n => //= n IHn; rewrite suml_cons.
(*D*)rewrite suml_add2list IHn addnCA addnA.
(*D*)by rewrite -(addn1 n) sqrnD size_odds muln1.
(*A*)Qed.
(**
#
#
#
#
#
(hint)
#
For [eq_suml_odds], use [sqrnD]
#

#
#

#
#
#

----------------------------------------------------------
#
#

*** Exercise 4:

Prove the sum of the lists [odds n] is what you think.

You may want to have at least one itermediate lemma to prove [oddsE]
#
#
*)
Lemma oddsE n : odds n = [seq 2 * i + 1 | i <- iota 0 n].
Proof.
(*D*)rewrite /odds; set k := (0 as X in iota X _).
(*D*)rewrite -[1 in LHS]/(2 * k + 1).
(*D*)elim: n k => //= n IHn k; rewrite {}IHn; congr (_ :: _).
(*D*)by elim: n k => // n IHn k /=; rewrite IHn !mulnS.
(*A*)Qed.
(**
#
#
#
#
#
(hint)
#
this intermediate lemma would be:
#
#
*)
Lemma oddsE_aux n k :
  iter n (fun s : seq nat => 2 * k + 1 :: add2list s) [::] =
  [seq 2 * i + 1 | i <- iota k n].
(*D*)Proof.
(*D*)elim: n k => //= n IHn k; rewrite {}IHn; congr (_ :: _).
(*D*)by elim: n k => // n IHn k /=; rewrite IHn !mulnS.
(*A*)Qed.
(**
#
#
#

#
#
#
#
#
*)
Lemma nth_odds n i : i < n -> nth 0 (odds n) i = 2 * i + 1.
Proof.
(*D*)by move=> i_ltn; rewrite oddsE (nth_map 0) ?size_iota ?nth_iota.
(*A*)Qed.
(**
#
#
#

#
#
#

----------------------------------------------------------
#
#

*** Exercise 5:

Let us prove directly formula
#$$ \sum_{i=0}^{n-1} (2 i + 1) = n ^ 2 $$#
from lesson 1, slightly modified.

Let us first define a custom sum operator:
#
#
*)
Definition mysum m n F := (foldr (fun i a => F i + a) 0 (iota m (n - m))).

Notation "\mysum_ ( m <= i < n ) F" := (mysum m n (fun i => F))
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \mysum_ ( m  <=  i  <  n ) '/  '  F ']'").
(**
#
#
- First prove a very useful lemma about summation
#
#
*)
Lemma mysum_recl m n F : m <= n ->
  \mysum_(m <= i < n.+1) F i = \mysum_(m <= i < n) F i + F n.
Proof.
(*D*)move=> leq_mn; rewrite /mysum subSn// -addn1 iota_add subnKC//= foldr_cat/=.
(*D*)by elim: (iota _ _) (F n) => [|x s IHs] k //=; rewrite IHs addnA.
(*A*)Qed.
(**
#
#
- Now prove the main result

Do NOT use [eq_suml_odds] above, it would take much more time

#
#
*)
Lemma sum_odds n : \mysum_(0 <= i < n) (2 * i + 1) = n ^ 2.
Proof.
(*D*)elim: n => // n IHn; rewrite mysum_recl// IHn.
(*D*)by rewrite -[n.+1]addn1 sqrnD muln1 addnAC addnA.
(*A*)Qed.
(**
#
#
#

#
#
#
*)

author: gares