text:
Require Import Utf8.
Require Import IxFree.Base IxFree.BinaryFixpoint.

Require Import Arith.
Require Import Omega.

Definition IRel_3 {A B : Type} (P : A → B → Type) := ∀ x, IRel_2 (P x).
Definition True_3 {A B : Type} {P : A → B → Type} : IRel_3 P := λ _, True_2.

Program Definition contractive_3 {A B : Type} {P : A → B → Type} (f : IRel_3 P → IRel_3 P) :=
  ∀ (n : nat) (R₁ R₂ : IRel_3 P),
  (∀ k, k < n → ∀ x y z, (k ⊨ R₁ x y z) <-> (k ⊨ R₂ x y z)) →
  ∀ x y z, (n ⊨ f R₁ x y z) <-> (n ⊨ f R₂ x y z).

Fixpoint pow_IRel_3 {A B : Type} {P : A → B → Type}
    (f : IRel_3 P → IRel_3 P) (n : nat) (R₀ : IRel_3 P) :=
  match n with
  | 0   => R₀
  | S n => f (pow_IRel_3 f n R₀)
  end.

Lemma pow_IRel_3_limit {A B : Type} {P : A → B → Type} (f : IRel_3 P → IRel_3 P) :
  contractive_3 f → ∀ k n m : nat, k ≤ n → k ≤ m → ∀ x y z,
  ((k ⊨ f (pow_IRel_3 f n True_3) x y z) <->
   (k ⊨ f (pow_IRel_3 f m True_3) x y z)).
Proof.
  intro Hcon.
  apply (well_founded_ind lt_wf (λ k, ∀ n m, k ≤ n → k ≤ m → ∀ x y z, (_ : Prop))).
  intros k HI n m H₁ H₂ x y z ; destruct k.
  + apply Hcon ; intros ; omega.
  + apply Hcon ; intros l Hl.
    destruct n ; [ exfalso ; omega | ].
    destruct m ; [ exfalso ; omega | ].
    apply HI ; omega.
Qed.

Definition I_fix_3_func {A B : Type} {P : A → B → Type} (f : IRel_3 P → IRel_3 P) :
    ∀ x y, P x y → nat → Prop :=
  λ x y z n, n ⊨ f (pow_IRel_3 f n True_3) x y z.

Lemma I_fix_3_func_monotone {A B : Type} {P : A → B → Type} (f : IRel_3 P → IRel_3 P) :
  contractive_3 f → ∀ x y z, monotone (I_fix_3_func f x y z).
Proof.
  intros Hcon x y z n ; induction n.
  + unfold I_fix_3_func ; simpl.
    intro H₁; apply (Hcon 0 True_3 (f True_3)).
    - intros k H; inversion H.
    - apply I_valid_monotone_S; assumption.
  + unfold I_fix_3_func.
    intro H₁; apply (Hcon (S n)
        (pow_IRel_3 f (S n) True_3) (pow_IRel_3 f (S (S n)) True_3)).
    - intros; apply pow_IRel_3_limit; trivial; omega.
    - apply I_valid_monotone_S; assumption.
Qed.

Definition I_fix_3 {A B : Type} {P : A → B → Type} (f : IRel_3 P → IRel_3 P) (p : contractive_3 f) :
  IRel_3 P :=
  λ x y z, mk_IProp (I_fix_3_func f x y z) (I_fix_3_func_monotone f p x y z).

Lemma I_fix_3_is_fixpoint {A B : Type} {P : A → B → Type}
  (f : IRel_3 P → IRel_3 P) (p : contractive_3 f) :
  ∀ x y z n, (n ⊨ I_fix_3 f p x y z) <-> (n ⊨ f (I_fix_3 f p) x y z).
Proof.
  intros x y z n; apply iff_trans with (B := (n ⊨ f (pow_IRel_3 f n True_3) x y z)).
  { split; intro H; [ apply I_valid_elim in H | apply I_valid_intro ]; auto. }
  apply p; intros k Hle x' y' z'.
  destruct n; [ omega | ]; simpl.
  apply iff_trans with (B := (k ⊨ f (pow_IRel_3 f k True_3) x' y' z')).
  { apply pow_IRel_3_limit; trivial; omega. }
  split; intro H; [ apply I_valid_intro | apply I_valid_elim in H ]; auto.
Qed.

Lemma I_fix_3_unroll {A B : Type} {P : A → B → Type}
  (f : IRel_3 P → IRel_3 P) (p : contractive_3 f) :
  ∀ x y z n, (n ⊨ I_fix_3 f p x y z) → (n ⊨ f (I_fix_3 f p) x y z).
Proof.
apply I_fix_3_is_fixpoint.
Qed.

Lemma I_fix_3_roll {A B : Type} {P : A → B → Type}
  (f : IRel_3 P → IRel_3 P) (p : contractive_3 f) :
  ∀ x y z n, (n ⊨ f (I_fix_3 f p) x y z) → (n ⊨ I_fix_3 f p x y z).
Proof.
apply I_fix_3_is_fixpoint.
Qed.

author: yizhouzhang

repo: ixfree

save_path: github-repos/coq/yizhouzhang-ixfree


text:
Require Export Adjoint.
Require Import Notations Common FunctorCategoryFunctorial Duals TypeclassSimplification.

Set Implicit Arguments.

Generalizable All Variables.

Set Asymmetric Patterns.

Set Universe Polymorphism.

Section AdjointPointwise.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).
  Context `(E : @SpecializedCategory objE).
  Context `(C' : @SpecializedCategory objC').
  Context `(D' : @SpecializedCategory objD').

  Variable F : SpecializedFunctor C D.
  Variable G : SpecializedFunctor D C.

  Variable A : Adjunction F G.
  Let A' : AdjunctionUnitCounit F G := A.

  Variables F' G' : SpecializedFunctor C' D'.

(*  Variable T' : SpecializedNaturalTransformation F' G'.*)

  Definition AdjointPointwise_NT_Unit : SpecializedNaturalTransformation (IdentityFunctor (C ^ E))
                                                                    (ComposeFunctors (G ^ IdentityFunctor E) (F ^ IdentityFunctor E)).
    clearbody A'; clear A.
    pose proof (A' : AdjunctionUnit _ _) as A''.
    refine (NTComposeT _ (LiftIdentityPointwise _ _)).
    refine (NTComposeT _ (projT1 A'' ^ (IdentityNaturalTransformation (IdentityFunctor E)))).
    refine (NTComposeT (LiftComposeFunctorsPointwise _ _ (IdentityFunctor E) (IdentityFunctor E)) _).
    refine (LiftNaturalTransformationPointwise (IdentityNaturalTransformation _) _).
    exact (LeftIdentityFunctorNaturalTransformation2 _).
  Defined.

  Definition AdjointPointwise_NT_Counit : SpecializedNaturalTransformation (ComposeFunctors (F ^ IdentityFunctor E) (G ^ IdentityFunctor E))
                                                                           (IdentityFunctor (D ^ E)).
    clearbody A'; clear A.
    pose proof (A' : AdjunctionCounit _ _) as A''.
    refine (NTComposeT (LiftIdentityPointwise_Inverse _ _) _).
    refine (NTComposeT (projT1 A'' ^ (IdentityNaturalTransformation (IdentityFunctor E))) _).
    refine (NTComposeT _ (LiftComposeFunctorsPointwise_Inverse _ _ (IdentityFunctor E) (IdentityFunctor E))).
    refine (LiftNaturalTransformationPointwise (IdentityNaturalTransformation _) _).
    exact (LeftIdentityFunctorNaturalTransformation1 _).
  Defined.

  Definition AdjointPointwise : Adjunction (F ^ (IdentityFunctor E)) (G ^ (IdentityFunctor E)).
    clearbody A'; clear A.
    match goal with
      | [ |- Adjunction ?F ?G ] =>
        refine (_ : AdjunctionUnitCounit F G)
    end.
    exists AdjointPointwise_NT_Unit
           AdjointPointwise_NT_Counit;
      simpl;
      abstract (
          destruct A';
          simpl in *;
            nt_eq;
          rsimplify_morphisms;
          try match goal with
                | [ H : _ |- _ ] => apply H
              end
        ).
  Defined.
End AdjointPointwise.

author: CategoricalData

repo: catdb

save_path: github-repos/coq/CategoricalData-catdb


text:
(* PREAMBLE *)

From compcert.cfrontend Require Csyntax Csem.
From compcert.lib Require Coqlib.

From trancert.analysis Require Function.
From trancert.lib Require List.

Import lib.All Csyntax Csem List Coqlib common.AST cfrontend.Ctypes analysis.Function Decidability.

Local Notation program := Csyntax.program.
Local Notation type := Ctypes.type.
Local Notation ident := AST.ident.
Local Notation fundef := Csyntax.fundef.
Local Notation globvar := (AST.globvar type).
Local Notation gdef := (AST.globdef (Ctypes.fundef function) type ).
Local Notation Internal := Ctypes.Internal.

(** *Properties of [program] *)

(** Conversion between [Ctypes.prog_defs] and [AST.prog_defs]. *)
Lemma ctypes_to_ast_prog_defs:
  forall (p:program), Ctypes.prog_defs p = AST.prog_defs (Ctypes.program_of_program p).
Proof. intros []; auto. Defined.

(** * Well-formedness of AST*)

(** CompCert has an unverified parser which is not formalized in Coq.
    The type of AST yielded by the parser allows for construction of such trees that
    are never produced by the parser (but might occur as a result of reductions). In
    this file we formalize the constraints on the AST that we require in our proofs
    and provide computable functions to verify them; this way we can validate the
    AST before doing refactoring and fail if the constraints are not satisfied.
 *)

Section DistinctIdentifiers.

  (** **Distinct Identifiers *)

  (** In [program], all identifiers are distinct. This is not enforced by construction, but parser works this way. *)

  (** In our proofs we rely on this fact, so as a part of code transformation we
      will validate this property and fail if it does not hold. *)
  Definition program_idents_wf (p:Csyntax.program) : Prop :=
    list_norepet (List.map fst (Ctypes.prog_defs p)) .

  Theorem program_idents_wf_dec (p: Csyntax.program) :
    { program_idents_wf p } +  { ~ program_idents_wf p }.
  Proof.
    apply list_norepet_dec. apply peq.
  Defined.

End DistinctIdentifiers.

Section ProgramWF.

  (** * Program well-formedness *)

  (** In this section we collect everything we know about parser output. *)

  Inductive globdef_wf : globdef (Csyntax.fundef) type -> Prop :=
  | gdwf_var:
      forall v, globdef_wf  (Gvar v)

  | gdwf_fundef :
      forall f, fundef_wf f -> globdef_wf (Gfun f)
  .

  Theorem globdef_wf_dec :
    forall g, dec (globdef_wf g).
  Proof.
    destruct g; try solve [repeat constructor].
    destruct (fundef_wf_dec f).
    {
      repeat constructor; assumption.
    }
    {
      constructor 2. contradict n. inversion n. assumption.
    }
  Defined.

  Record program_wf (p:Csyntax.program) : Prop :=
    {
    pwf_idents: program_idents_wf p ;
    pwf_defs:   Forall (skip1 globdef_wf) (Ctypes.prog_defs p)
    } .

  Theorem program_wf_dec :
    forall p, dec (program_wf p).
  Proof.
    assert (H:forall e : ident * globdef Csyntax.fundef type, dec (skip1 globdef_wf e)).
    {
      clear.
      intros e.
      destruct e.
      simpl in *.
      destruct (globdef_wf_dec g).
      {
        constructor 1.
        assumption.
      }
      {
        constructor 2.
        contradict n. assumption.
      }
    }

    intros p.
    destruct (program_idents_wf_dec p), p;
      destruct (Forall_decidability (skip1 globdef_wf) H prog_defs);
      try solve [constructor 1; constructor; auto
                |
                constructor 2; contradict n; inv n; auto
                ].
  Defined.

(** ** Identifiers in a well-formed program *)

  Import Globalenvs.Genv.

Definition def_id (p: program) (def: AST.globdef _ _) (id:AST.ident): Prop :=
  In (id, def) (Ctypes.prog_defs p).

Definition fundef_id (p: program) (f: fundef) (id:AST.ident): Prop :=
  def_id p (AST.Gfun f) id.

Definition fun_id (p: Csyntax.program) (f: function) (id:AST.ident): Prop :=
  fundef_id p (Ctypes.Internal f) id.

Definition genv_def_id (ge:genv) def (id: AST.ident): Prop :=
  exists b, (genv_defs ge) ! b = Some def /\ (genv_symb ge) ! id = Some b.

Definition genv_fundef_id (ge:genv) (f: fundef) (id: AST.ident): Prop :=
  genv_def_id ge (AST.Gfun f) id.

Theorem fundef_id_inj :
  forall f1 f2 p i,
    program_wf p ->
    fundef_id p f1 i ->
    fundef_id p f2 i -> f1 = f2.
Proof.
  unfold fundef_id, def_id; intros.
  inv H.
  unfold program_idents_wf in *.
  eapply in_norepet_unique2 in H0; eauto.
  decomp.
  rewrite -> H in *.
  apply in_app in H1.
  decomp.
  - apply (in_map fst) in H1. contradiction.
  - destruct H1; last by  apply (in_map fst) in H1.
      by inv H1.
Qed.

Theorem fun_id_inj :
  forall f1 f2 p i,
    program_wf p ->
    fun_id p f1 i ->
    fun_id p f2 i -> f1 = f2.
Proof.
  move => ? ? ? ? Hwf H1 H2.
  by move: (fundef_id_inj _ _ _ _ Hwf H1 H2); inversion 1.
Qed.

Section Genv.
  Import Globalenvs.Genv.

  Theorem prog_def_id_genv:
    forall (p:Csyntax.program),
      list_norepet (AST.prog_defs_names (Ctypes.program_of_program p)) ->
      forall def id, (def_id p def id <-> genv_def_id (Csem.globalenv p) def id).
  Proof.
    split; unfold fundef_id, def_id, genv_fundef_id, genv_def_id.
    {
      move: ctypes_to_ast_prog_defs -> =>
      /AST.prog_defmap_norepet /Globalenvs.Genv.find_def_symbol.
      unfold find_symbol, find_def.
      intros (b & Hsym & Hdef) =>//.
      change (Csyntax.fundef) with (Ctypes.fundef function) in *.
      eauto.
    }
    {
      intros (b & Hsym & Hdef) =>//.
      change (Csyntax.fundef) with (Ctypes.fundef function) in *.
      simpl in *.
      move: ctypes_to_ast_prog_defs -> .
      eapply AST.in_prog_defmap.
      apply find_def_symbol; eauto.
    }
  Qed.

  Theorem prog_fundef_id_genv:
    forall (p:Csyntax.program),
      list_norepet (AST.prog_defs_names (Ctypes.program_of_program p)) ->
      (forall f id, fundef_id p f id <-> genv_fundef_id (Csem.globalenv p) f id).
  Proof.
    split; by apply prog_def_id_genv.
  Qed.

  Lemma fundef_id_exists:
    forall (p:program) fd vf,
      program_wf p ->
      let ge := Csem.globalenv p in
      (forall b def, (genv_defs ge) ! b = Some def -> exists i : positive, (genv_symb ge) ! i = Some b) ->
      find_funct ge vf = Some fd -> exists fdfid, fundef_id p fd fdfid.
  Proof.
    intros.
    assert (exists fdfid, genv_fundef_id (Csem.globalenv p) fd fdfid) as (fdfid & Hfdfid).
    {
      unfold find_funct, find_funct_ptr, find_symbol, find_def, genv_fundef_id, genv_def_id in *.
      intros.
      repeat option_cases.
      subst.
      autoinj.
      edestruct H0 as (i & Hsymb); eauto.
    }
    exists fdfid.
    apply prog_fundef_id_genv; auto.
    by inv H.
  Qed.

End Genv.
End ProgramWF.

(* Section DistinctFunctions. *)

(*   (** * Distinct global identifiers *) *)

(*   (** This is not a well-formed-ness condition, but a condition required to *)
(*   conduct some proofs. If functions are not distinct we can not differentiate *)
(*   between them once their identifiers are lost -- e.g. in continuations. *) *)

(*   Definition distinct_functions (p: program) : Prop := *)
(*     forall (i j:ident) f, *)
(*       In (i, Gfun f) (prog_defs p) -> *)
(*       In (j, Gfun f) (prog_defs p) -> *)
(*       i = j . *)

(*   (** *)
(*      Suppose [program_idents_wf p] holds. Let us construct an initial global *)
(*      environment [ge] from it. If [genv_defs ge] holds a definition by an *)
(*      address [b], then there exists a symbol [id] that is mapped to this *)
(*      address. *)
(*   *) *)

  Import Globalenvs Genv.
  Import compcert.lib.Maps Maps.PTree common.Values.

  Theorem symb_exists:
    forall (b:block) (p:program) def,
      let ge := Genv.globalenv p in

      program_idents_wf p ->

      (genv_defs ge) ! b = Some def ->
      exists id, (genv_symb ge) ! id = Some b.
  Proof.
    unfold globalenv,program_idents_wf.
    intros b [] def Hidents Hget =>//=.
    pose (P := fun ge => get b (genv_defs ge) = Some def -> exists id, get id (genv_symb ge) = Some b).
    assert (REC: forall l ge,
               list_norepet (List.map fst l) ->
               (forall i, In i (List.map fst l) -> get i (genv_symb ge) = None) ->
               P ge ->
               P (add_globals ge l)).
    {
      elim =>//=.
      intros [] l IHl ge. inversion 1 => Hcond HP Hdef.
      apply IHl; auto.
      - move => i Hget'  //=.
        move: gsspec ->; simpl in *; subst.
        erewrite Hcond; eauto.
        destruct (peq _ _); [subst; contradiction| auto].
      - red. red in HP.
        simpl in *.
        move: gsspec =>->.
        destruct (peq _ _).
        + inversion 1. subst.
          exists p. apply gss.
        + move => /HP. intros [id Hid].
          exists id. rewrite gsspec.
          destruct (peq _ _ ); auto.
          subst.
          erewrite Hcond in Hid; [discriminate| eauto 2].
    }
    apply REC; eauto.
    - by intros; apply gempty.
    - by red; rewrite gempty.
  Qed.

  Lemma wf_globalenv_ident:
    forall p id g,
      program_idents_wf p ->
      In (id, g) (prog_defs p) ->
      exists b, find_symbol (globalenv p) id = Some b /\ find_def (globalenv p) b = Some g.
  Proof.
    intros p id g H H0.
    unfold program_idents_wf  in *.
    rewrite ctypes_to_ast_prog_defs in H.
    exploit AST.prog_defmap_norepet; eauto.
    by move / find_def_symbol.
  Qed.

  (* Theorem fundef_id_unique: *)
  (*   forall f i1 i2 p, *)
  (*     program_wf p -> *)
  (*     distinct_functions p -> *)
  (*     fundef_id p f i1 -> fundef_id p f i2 -> i1 = i2. *)
  (* Proof. by intros; eauto. Qed. *)

author: sayon

repo: trancert

save_path: github-repos/coq/sayon-trancert


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*{ extras :  Equality\_structures.v }%*)
Set Implicit Arguments.
Unset Strict Implicit.
Require Export seq_equality_facts.

(** - This is a rather experimental file.
 - Remember how we defined not only a setoid of sequences (seq n A)
 for each n:nat and A:Setoid, but also a new equality predicate seq_equal
 spanning all sequences over A. Perhaps we can generalize this idea:
 in a setoid, the equality comes with the definition of the setoid, which
 is in a sense "prior" to the equality; we have no equality unless we
 have a setoid. Here I try to reverse things by defining a predicate
 spanning many setoids that has some nice properties, such as being
 refl, symm, and trans, and nicely restricts to, and extends the setoid
 equalities just like seq_equal *)

Section defs.
Variable A : Setoid.
Variable I : A -> Setoid.
Definition StrEqType := forall a b : A, I a -> I b -> Prop.
Record EqStructure : Type :=
  {StrEq :> forall a b : A, I a -> I b -> Prop;
   StrEqRefl : forall (a : A) (x : I a), StrEq x x;
   StrEqSym :
    forall (a b : A) (x : I a) (y : I b), StrEq x y -> StrEq y x;
   StrEqTrans :
    forall (a b c : A) (x : I a) (y : I b) (z : I c),
    StrEq x y -> StrEq y z -> StrEq x z;
   StrEqRestr : forall (a : A) (x y : I a), StrEq x y -> x =' y in I a;
   StrEqExtend : forall (a : A) (x y : I a), x =' y in I a -> StrEq x y;
   StrEqIndex :
    forall (a b : A) (x : I a) (y : I b), StrEq x y -> a =' b in A}.
End defs.

Definition seq_eq_str (A : Setoid) : EqStructure (fun n : Nat => seq n A).
apply
 (Build_EqStructure (I:=fun n : Nat => seq n A)
    (StrEq:=fun (n m : Nat) (v : seq n A) (w : seq m A) => seq_equal v w));
 auto with algebra.
intros.
apply seq_equal_trans with (w := y); auto with algebra.
2: intros.
2: simpl in |- *.
2: apply seq_equal_length_equal with (v := x) (w := y); auto with algebra.
simpl in |- *.
intros; red in H; red in |- *; simpl in H; simpl in |- *.
intros.
elim (le_or_lt a i).
right.
auto.
left.
exists H0; exists H0.
auto.
Defined.

Definition fin_eq_str : EqStructure (fun n : Nat => fin n).
apply
 (Build_EqStructure (I:=fun n : Nat => fin n)
    (StrEq:=fun n m (i : fin n) (j : fin m) => n = m /\ index i = index j));
 auto with algebra.
intros.
intuition.
intuition.
transitivity b; auto.
transitivity (index y); auto.
intros.
simpl in |- *.
inversion_clear H.
auto.
intros.
simpl in |- *.
inversion_clear H.
rewrite H0.
auto.
Defined.

Definition fin_eq := StrEq fin_eq_str.

Lemma test1 : forall (n : nat) (i : fin n), fin_eq i i.
intros.
red in |- *.
simpl in |- *.
split; auto.
Qed.

Definition seq_eq (A : Setoid) := StrEq (seq_eq_str A).

Lemma test2 :
 forall (A : Setoid) (n m : nat) (v : seq n A) (w : seq m A),
 seq_eq v w -> seq_eq w v.
intros.
red in |- *.
simpl in |- *.
red in H; simpl in H.
auto with algebra.
Qed.

(** - Somthing I'd like to do is somehow enable EqStructures to span setoids indexed
 by more than one setoid; something like [MatEqStr : (EqStructure [n,m:Nat](matrix F n m))]
 instead of (modulo correction of notation) [MatEqStr : (EqStructure
 [nm:(cartesian_prod Nat Nat)](matrix F (pi1 nm) (pi2 nm)))] *)

author: coq-contribs

repo: lin-alg

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


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

(*i $Id: NZProperties.v 14641 2011-11-06 11:59:10Z herbelin $ i*)

Require Export NZAxioms NZMulOrder.

(** This functor summarizes all known facts about NZ.
    For the moment it is only an alias to [NZMulOrderPropFunct], which
    subsumes all others.
*)

Module Type NZPropFunct := NZMulOrderPropSig.

author: JasonGross

repo: category-coq-experience-tests


text:
(* Consigne générale: structurer proprement vos scripts de preuve;
   chaque fois qu'une tactique produit plus d'un but, utiliser des
   puces pour séparer les preuves des deux buts.

   Vous pouvez aussi essayer, autant que possible, d'enchaîner les
   tactiques au moyen de points-virgules.
*)

(* Tous les "Admitted" doivent être remplacés par vos scripts de preuves. *)

(* Quelques lemmes à prouver *)
Section Complements_Negation.
Variables P Q R S: Prop.

Lemma contraposee: (P->Q) -> (~Q->~P).
Proof.
   intros.
   unfold not.
   intro.
   unfold not in H0.
   apply H0.
   apply H.
   assumption.
Qed.

Lemma autre_contraposee: (P->~Q) -> (Q->~P).
Proof.
   unfold not.
   intros.
   apply H.
   assumption.
   assumption.
Qed.

Lemma DS1: ((P->Q)->R)->((~P->~Q)->~R)->(P->Q->S).
Proof.
   unfold not.
   intros.
   exfalso.
   apply H0.
   intros.
   apply H3.
   assumption.
   apply H.
   intro.
   assumption.
Qed.

Lemma DS2: (P->Q)->~(R->Q)->(~R->S) -> (R->P->S).
Proof.
   unfold not.
   intros.
   apply H1.
   intro.
   apply H0.
   intro.
   apply H.
   assumption.
Qed.

(* Ne pas foncer sans réfléchir *)
Lemma piege: (P->~Q)->(~Q->R)->(R->~S)->(~S->~P) -> ~P.
Proof.
   intros.
   unfold not.
   intro.
   apply H1.
   apply H0.
   apply H.
   assumption.
   exfalso.
   apply H2.
   apply H1.
   apply H0.
   apply H.
   assumption.
   assumption.
(* à compléter *)
Qed.

End Complements_Negation.

Section Double_Negation.
(* Autour de la double négation *)
Variables P Q: Prop.
(* De P, on peut déduire non-non-P *)
Lemma dn_i: P-> ~~P.
Proof.
   intro.
   unfold not.
   intro.
   apply H0.
   assumption.
Qed.

(* On a prouvé dans absurd' (fichier negation.v), que, de "non-P implique P",
   on peut déduire, peut-être pas P, mais au moins non-non-P *)

(* Si on suppose, ce qui est plus fort, qu'on peut déduire P
   de "non-P implique P", alors on peut justifier l'élimination de
   la double négation [pour P] *)
Lemma trop_de_negations: ((~P->P)->P) -> (~~P -> P).
Proof.
   intros.
   apply H.
   intro.
   exfalso.
   unfold not in H0.
   apply H0.
   unfold not in H1.
   assumption.
Qed.

End Double_Negation.

Section Preuves_de_sequents.
Variables P Q R S: Prop.
(* Les exercices restants consistent à formuler soi-même les lemmes:
   chaque séquent à prouver va constituer une sous-section, avec ses
   hypothèses *)

(* Et bien sûr, faire la preuve ensuite! *)

(* Exemple *)
  Section Exemple.
  (* Séquent à prouver: P->Q, P->~Q |- P->R *)
  Hypothesis H: P->Q.
  Hypothesis H1: P->~Q.
  Lemma exemple: P->R.
  Proof.
  intro p. exfalso.
  apply H1.
  - assumption.
  - apply H. assumption.
  Qed.
  End Exemple.

  Section Sequent1.
  (* Séquent à prouver:
     (P->Q)->~Q |- (P->Q)->~P
  *)
  Hypothesis H: (P->Q)->~Q.
  Lemma Sequent1: (P->Q)->~P.
  Proof.
   intro.
   unfold not.
   intro.
   unfold not in H.
   apply H.
   - assumption.
   - apply H0. assumption.
   Qed.
  End Sequent1.

  Section Sequent2.
  (* Séquent à prouver:
     (P->Q)->R, (P->Q)->~R |- Q->S
  *)
  Hypothesis H: (P->Q)->R.
  Hypothesis H0: (P->Q)->~R.
  Lemma Sequent2: Q->S.
  Proof.
   intro.
   unfold not in H0.
   exfalso.
   apply H0.
   -intro. assumption.
   -apply H. intro. assumption.
  Qed.

  End Sequent2.

  Section Sequent3.
  (* Séquent à prouver:
     P->Q, ~P->Q |- ~~Q
  *)
  Hypothesis H: P->Q.
  Hypothesis H0: ~P->Q.
  Lemma Sequent2: ~~Q.
  Proof.
   unfold not.
   intro.
   apply H1.
   apply H0.
   intro.
   apply H1.
   apply H.
   assumption.
  Qed.
  End Sequent3.

End Preuves_de_sequents.

author: Anatgnr

repo: Logique-et-Preuve


text:
Require Export low_mods.

Fixpoint is_neg_SO_pre (alpha : SecOrder) (i : nat) : bool :=
  match alpha with
    predSO _ _  => false
  | relatSO _ _  => false
  | eqFO _ _  => false
  | allFO _  beta => is_neg_SO_pre beta i
  | negSO beta => negb (is_neg_SO_pre beta i)
  | exFO _  beta => is_neg_SO_pre beta i
  | conjSO beta1 beta2 => if le_dec i (length (preds_in beta1)) then is_neg_SO_pre beta1 i
                          else is_neg_SO_pre beta2 (i-(length (preds_in beta1)))
  | disjSO beta1 beta2 => if le_dec i (length (preds_in beta1)) then (is_neg_SO_pre beta1 i)
                          else is_neg_SO_pre beta2 (i-(length (preds_in beta1)))
  | implSO beta1 beta2 => if le_dec i (length (preds_in beta1)) then negb (is_neg_SO_pre beta1 i)
                          else is_neg_SO_pre beta2 (i-(length (preds_in beta1)))
  | allSO _ beta => match i with
                                     | 0 => false
                                     | S 0 => false
                                     | S j => is_neg_SO_pre beta j
                                     end
  | exSO _ beta => match i with
                                     | 0 => false
                                     | S 0 => false
                                     | S j => is_neg_SO_pre beta j
                                     end
  end.

Definition is_neg_SO alpha i : Prop :=
occ_in_SO alpha i /\ is_neg_SO_pre alpha i = true.
(*
Inductive is_neg_SO alpha i : Prop :=
| occ_neg_SO : occ_in_SO alpha i -> is_neg_SO_pre alpha i = true -> is_neg_SO alpha i.
*)

author: caitlindabrera

repo: Sahlqvist


Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Specific.solinas32_2e452m3_17limbs.Synthesis.

(* TODO : change this to field once field isomorphism happens *)
Definition mul :
  { mul : feBW_loose -> feBW_loose -> feBW_tight
  | forall a b, phiBW_tight (mul a b) = F.mul (phiBW_loose a) (phiBW_loose b) }.
Proof.
  Set Ltac Profiling.
  Time synthesize_mul ().
  Show Ltac Profile.
Time Defined.

Print Assumptions mul.


text:
(* Code from https://github.com/tchajed/coq-record-update *)
Set Implicit Arguments.

(** Reader is the reader monad (or just the function monad). We only use
Applicative here. *)
Definition Reader E T := forall (e:E), T e.
Arguments Reader : clear implicits.

(* pure/return *)
Definition constructor {E T} (x:T) : Reader E (fun _ => T) := fun _ => x.

(* Always unfold when applied with a "final" argument.
Before this: Eval cbn in (constructor 5 0) gives 'constructor 5 0'
After this: Eval cbn in (constructor 5 0) gives '5' *)
Arguments constructor {_ _} _ _ /.

(* Applicative's (<*>) (written as `ap`).

This has an awkwardly long name since it's intended to be used infix with
 *)
Definition applicative_ap {E}
           {A: E -> Type}
           {B: forall (e:E), A e -> Type}
           (f: Reader E (fun e => forall (a:A e), B e a)) :
  forall (x: Reader E A), Reader E (fun e => B e (x e))  :=
  fun x => fun e => f e (x e).

(** Settable is a way of accessing a constructor for a record of type T. The
syntactic form of this definition is important: it must be an eta-expanded
version of T's constructor, written generically over the field accessors of T.
The best way to do this for a record X := mkX { A; B; C} is
[settable! mkX <A; B; C>]. *)
Class Settable T := { mkT: Reader T (fun _ => T);
                      mkT_ok: forall x, mkT x = x }.
Arguments mkT T mk : clear implicits, rename.

Local Ltac solve_mkT_ok :=
  match goal with
  | |- forall x, _ = _ => solve [ destruct x; cbv; f_equal ]
  end.

(** settable! creates an instance of Settable from a constructor and list of
fields. *)
Notation "'settable!' mk < f1 ; .. ; fn >" :=
  (Build_Settable
     (applicative_ap .. (applicative_ap (constructor mk) f1) .. fn)
     ltac:(solve_mkT_ok)) (at level 0, mk at level 10, f1, fn at level 9, only parsing).

(** [setter] creates a setter based on an eta-expanded record constructor and a
particular field projection proj *)
Local Ltac setter etaT proj :=
  lazymatch etaT with
  | context[proj] => idtac
  | _ => fail 1 proj "is not a field"
  end;
  let set :=
      (match eval pattern proj in etaT with
       | ?setter ?proj => constr:(fun f => setter (fun r => f (proj r)))
       end) in
  let set := (eval cbv [constructor applicative_ap] in set) in
  exact set.

(* Combining the above, [getSetter'] looks up the eta-expanded version of T with
the Settable typeclass, and calls [setter] to create a setter. *)
Local Ltac get_setter T proj :=
  match constr:(mkT T _) with
  | mkT _ ?updateable =>
    let updateable := (eval hnf in updateable) in
    match updateable with
    | {| mkT := ?mk |} =>
      setter mk proj
    end
  end.

(* Setter provides a way to change a field given by a projection function, along
with correctness conditions that require the projected field and only the
projected field is modified. *)
Class Setter {R T} (proj: R -> T) := set : (T -> T) -> R -> R.
Arguments set {R T} proj {Setter}.

Class SetterWf {R T} (proj: R -> T) :=
  { set_wf :> Setter proj;
    set_get: forall v r, proj (set proj v r) = v (proj r);
    set_eq: forall f r, f (proj r) = proj r -> set proj f r = r; }.

Arguments set_wf {R T} proj {SetterWf}.

Local Ltac SetterInstance_t :=
  match goal with
  | |- @Setter ?T _ ?A => get_setter T A
  end.

Local Ltac SetterWfInstance_t :=
  match goal with
  | |- @SetterWf ?T _ ?A =>
    unshelve notypeclasses refine (Build_SetterWf _ _ _);
    [ get_setter T A |
      let r := fresh in
      intros ? r; destruct r; reflexivity |
      let f := fresh in
      let r := fresh in
      intros f r; destruct r; cbv; congruence ]
  end.

Hint Extern 1 (Setter _) => SetterInstance_t : typeclass_instances.
Hint Extern 1 (SetterWf _) => SetterWfInstance_t : typeclass_instances.

Module RecordSetNotations.
  Delimit Scope record_set with rs.
  Open Scope rs.
  Notation "x <| proj  :=  v |>" := (set proj (fun _ => v) x)
                                    (at level 12, left associativity) : record_set.
  Notation "x <| proj  ::=  f |>" := (set proj f x)
                                     (at level 12, f at next level, left associativity) : record_set.
  Notation "x <| proj1 ; proj2 ; .. ; projn := v |>" :=
    (set proj1 (set proj2 .. (set projn (fun _ => v)) ..) x)
    (at level 12, left associativity) : record_set.
  Notation "x <| proj1 ; proj2 ; .. ; projn ::= f |>" :=
    (set proj1 (set proj2 .. (set projn f) ..) x)
    (at level 12, f at next level, left associativity) : record_set.
End RecordSetNotations.

author: PLSysSec

repo: veriwasm-verification


text:
Require Import VST.floyd.proofauto.
Require Import common.
From SSL_VST Require Import core.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Inductive sll_card : Set :=
    | sll_card_0 : sll_card
    | sll_card_1 : sll_card -> sll_card.

Fixpoint sll (x: val) (s: (list Z)) (self_card: sll_card) {struct self_card} : mpred := match self_card with
    | sll_card_0  =>  !!((x : val) = nullval) && !!((s : list Z) = ([] : list Z)) && emp
    | sll_card_1 _alpha_522 =>
      EX v : Z,
      EX s1 : (list Z),
      EX nxt : val,
 !!(Int.min_signed <= v <= Int.max_signed) && !!(is_pointer_or_null nxt) && !!(~ ((x : val) = nullval)) && !!((s : list Z) = (([(v : Z)] : list Z) ++ (s1 : list Z))) && (data_at Tsh (tarray (Tunion _sslval noattr) 2) [(inl ((Vint (Int.repr v)) : val)); (inr (nxt : val))] (x : val)) * (sll (nxt : val) (s1 : list Z) (_alpha_522 : sll_card))
end.

Lemma sll_x_valid_pointerP x s self_card: sll x s self_card |-- valid_pointer x. Proof. destruct self_card; simpl; entailer;  entailer!; eauto. Qed.
Hint Resolve sll_x_valid_pointerP : valid_pointer.
Lemma sll_local_factsP x s self_card :
  sll x s self_card|-- !!(((((x : val) = nullval)) -> (self_card = sll_card_0))/\(((~ ((x : val) = nullval))) -> (exists _alpha_522, self_card = sll_card_1 _alpha_522))/\is_pointer_or_null((x : val))).
 Proof.  destruct self_card;  simpl; entailer; saturate_local; apply prop_right; eauto. Qed.
Hint Resolve sll_local_factsP : saturate_local.
Lemma unfold_sll_card_0  (x: val) (s: (list Z)) : sll x s (sll_card_0 ) =  !!((x : val) = nullval) && !!((s : list Z) = ([] : list Z)) && emp. Proof. auto. Qed.
Lemma unfold_sll_card_1 (_alpha_522 : sll_card) (x: val) (s: (list Z)) : sll x s (sll_card_1 _alpha_522) =
      EX v : Z,
      EX s1 : (list Z),
      EX nxt : val,
 !!(Int.min_signed <= v <= Int.max_signed) && !!(is_pointer_or_null nxt) && !!(~ ((x : val) = nullval)) && !!((s : list Z) = (([(v : Z)] : list Z) ++ (s1 : list Z))) && (data_at Tsh (tarray (Tunion _sslval noattr) 2) [(inl ((Vint (Int.repr v)) : val)); (inr (nxt : val))] (x : val)) * (sll (nxt : val) (s1 : list Z) (_alpha_522 : sll_card)). Proof. auto. Qed.

author: TyGuS

repo: ssl-vst

save_path: github-repos/coq/TyGuS-ssl-vst


text:
(* Copyright © 1998-2006
 * Henk Barendregt
 * Luís Cruz-Filipe
 * Herman Geuvers
 * Mariusz Giero
 * Rik van Ginneken
 * Dimitri Hendriks
 * Sébastien Hinderer
 * Bart Kirkels
 * Pierre Letouzey
 * Iris Loeb
 * Lionel Mamane
 * Milad Niqui
 * Russell O’Connor
 * Randy Pollack
 * Nickolay V. Shmyrev
 * Bas Spitters
 * Dan Synek
 * Freek Wiedijk
 * Jan Zwanenburg
 *
 * This work 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 2 of the License, or
 * (at your option) any later version.
 *
 * This work 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 this work; if not, write to the Free Software Foundation, Inc.,
 * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 *)

Require Export CoRN.algebra.COrdCauchy.
From Coq Require Import Lia.

Section Lemmas.

(**
* Lemmas for Integration

Here we include several lemmas valid in any ordered field [F] which
are useful for integration.

** Merging orders

We first prove that any two strictly ordered sets of points which have
an empty intersection can be ordered as one (this will be the core of
the proof that any two partitions with no common point have a common
refinement).
*)

Variable F : COrdField.

Lemma om_fun_lt : forall m n : nat, S m < S n -> m < n.
Proof.
 auto with zarith.
Qed.

Definition om_fun n m (f : forall i, i < n -> F) (g : forall i, i < m -> F)
  (Hfg : forall i j Hi Hj, f i Hi [#] g j Hj) : forall i, i < m + n -> F.
Proof.
 revert m f g Hfg. induction  n as [| n Hrecn].
  intros. apply (g i). rewrite <- plus_n_O in H; auto.
 intro m. induction  m as [| m Hrecm].
  do 3 intro. apply f.
 intros.
 elim (ap_imp_less _ _ _ (Hfg n m (lt_n_Sn n) (lt_n_Sn m))); intro.
  set (h := fun (i : nat) (Hi : i < m) => g i (lt_S _ _ Hi)) in *.
  elim (le_lt_eq_dec _ _ H); intro.
   apply Hrecm with (f := f) (g := h) (i := i); unfold h in |- *; auto.
   apply om_fun_lt; auto.
  apply (g m (lt_n_Sn m)).
 clear Hrecm.
 set (h := fun (i : nat) (Hi : i < n) => f i (lt_S _ _ Hi)) in *.
 elim (le_lt_eq_dec _ _ H); intro.
  apply Hrecn with (f := h) (g := g) (i := i); unfold h in |- *; auto.
  apply om_fun_lt. rewrite plus_n_Sm. auto.
 apply (f n (lt_n_Sn n)).
Defined.

Lemma om_fun_1 : forall n m f g Hfg,
 nat_less_n_fun f -> nat_less_n_fun g -> nat_less_n_fun (om_fun n m f g Hfg).
Proof.
 intro n. induction  n as [| n Hrecn].
 red in |- *; simpl in |- *; auto.
 intro m; induction  m as [| m Hrecm].
  red in |- *; simpl in |- *; auto.
 red in |- *; intros.
 simpl in |- *; elim ap_imp_less; simpl in |- *; intro;
   repeat (elim le_lt_eq_dec; simpl in |- *; intro); try (exfalso; auto with zarith; fail);
     try apply eq_reflexive_unfolded.
  set (h := fun (i : nat) (Hi : i < m) => g i (lt_S _ _ Hi)) in *.
  set (Hfh := fun i j Hi Hj => Hfg i j Hi (lt_S _ _ Hj)) in *.
  assert (Hh : nat_less_n_fun h). red in |- *; unfold h in |- *; auto.
   exact (Hrecm f h Hfh H Hh i j H1 (om_fun_lt _ _ a0) (om_fun_lt _ _ a1)).
 apply Hrecn; try red in |- *; auto.
Qed.

Lemma om_fun_2a : forall n m f g Hfg (x : F), (forall i Hi, f i Hi [<] x) ->
 (forall i Hi, g i Hi [<] x) -> forall i Hi, om_fun n m f g Hfg i Hi [<] x.
Proof.
 intro n. induction  n as [| n Hrecn].
 simpl in |- *; auto.
 intro m; induction  m as [| m Hrecm].
  simpl in |- *; auto.
 intros.
 simpl in |- *; elim ap_imp_less; simpl in |- *; intro; elim le_lt_eq_dec; simpl in |- *; intro; auto.
 set (h := fun (i : nat) (Hi : i < m) => g i (lt_S _ _ Hi)) in *.
 set (Hfh := fun i j Hi Hj => Hfg i j Hi (lt_S _ _ Hj)) in *.
 set (Hh := fun i Hi => X0 i (lt_S _ _ Hi)) in *.
 exact (Hrecm f h Hfh x X Hh i (om_fun_lt _ _ a0)).
Qed.

Lemma om_fun_2 : forall n m f g Hfg, nat_less_n_fun f -> nat_less_n_fun g ->
 (forall i i' Hi Hi', i < i' -> f i Hi [<] f i' Hi') -> (forall i i' Hi Hi', i < i' -> g i Hi [<] g i' Hi')
 -> forall i i' Hi Hi', i < i' -> om_fun n m f g Hfg i Hi [<] om_fun n m f g Hfg i' Hi'.
Proof.
 intro n. induction  n as [| n Hrecn].
 simpl in |- *; auto.
 intro m; induction  m as [| m Hrecm].
  simpl in |- *; auto.
 intros.
 simpl in |- *; elim ap_imp_less; simpl in |- *; intro;
   repeat (elim le_lt_eq_dec; simpl in |- *; intro); try (exfalso; auto with zarith; fail).
    set (h := fun (i : nat) (Hi : i < m) => g i (lt_S _ _ Hi)) in *.
    set (Hfh := fun i j Hi Hj => Hfg i j Hi (lt_S _ _ Hj)) in *.
    assert (Hh : nat_less_n_fun h). red in |- *; unfold h in |- *; auto.
     set (inch := fun i i' Hi Hi' Hii' => X0 i i' (lt_S _ _ Hi) (lt_S _ _ Hi') Hii') in *.
    exact (Hrecm f h Hfh H Hh X inch i i' (om_fun_lt _ _ a0) (om_fun_lt _ _ a1) H1).
   set (h := fun (i : nat) (Hi : i < m) => g i (lt_S _ _ Hi)) in *.
   set (Hfh := fun i j Hi Hj => Hfg i j Hi (lt_S _ _ Hj)) in *.
   assert (Hh : nat_less_n_fun h). red in |- *; unfold h in |- *; auto.
    refine (om_fun_2a _ _ f h Hfh (g m (lt_n_Sn m)) _ _ i (om_fun_lt _ _ a0)).
    intros j Hj. elim (le_lt_eq_dec _ _ Hj); intro.
    apply less_transitive_unfolded with (f n (lt_n_Sn n)); auto with arith.
    apply less_wdl with (f n (lt_n_Sn n)); auto.
    apply H; auto. inversion b0. auto.
    unfold h in |- *; auto.
  apply Hrecn; auto. red in |- *; auto.
  apply om_fun_2a; auto.
 intros j Hj. elim (le_lt_eq_dec _ _ Hj); intro.
 apply less_transitive_unfolded with (g m (lt_n_Sn m)); auto with arith.
 apply less_wdl with (g m (lt_n_Sn m)); auto.
 apply H0; auto. inversion b1. auto.
Qed.

Lemma om_fun_3a : forall n m f g Hfg, nat_less_n_fun f -> nat_less_n_fun g ->
 forall i Hi, {j : nat | {Hj : j < m + n | f i Hi [=] om_fun n m f g Hfg j Hj}}.
Proof.
 intro n. induction  n as [| n Hrecn].
 simpl in |- *; intros. exfalso; inversion Hi.
  intro m; induction  m as [| m Hrecm].
  simpl in |- *; intros. exists i. exists Hi. algebra.
  intros.
 simpl in |- *; elim ap_imp_less; simpl in |- *; intro.
  set (h := fun i Hi => g i (lt_S _ _ Hi)) in *.
  set (Hfh := fun i j Hi Hj => Hfg i j Hi (lt_S _ _ Hj)) in *.
  assert (Hh : nat_less_n_fun h). red in |- *; unfold h in |- *; auto.
   elim (Hrecm f h Hfh H Hh i Hi); intros j Hj.
  elim Hj; clear Hj; intros Hj Hj'.
  exists j; exists (lt_S _ _ Hj).
  elim le_lt_eq_dec; simpl in |- *; intro.
   astepl (om_fun _ _ f h Hfh _ Hj).
   refine (om_fun_1 _ _ f h Hfh H Hh j j _ Hj (om_fun_lt _ _ a0)). auto.
   exfalso; auto with zarith.
 elim (le_lt_eq_dec _ _ Hi); intro.
  set (h := fun i Hi => f i (lt_S _ _ Hi)) in *.
  set (Hfh := fun i j Hi Hj => Hfg i j (lt_S _ _ Hi) Hj) in *.
  assert (Hh : nat_less_n_fun h). red in |- *; unfold h in |- *; auto.
   elim (Hrecn _ h g Hfh Hh H0 i (om_fun_lt _ _ a)); intros j Hj.
  elim Hj; clear Hj; intros Hj Hj'.
  cut (j < S (m + S n)). intro. 2: auto with zarith.
   exists j; exists H1.
  elim le_lt_eq_dec; simpl in |- *; intro.
   eapply eq_transitive_unfolded. eapply eq_transitive_unfolded. 2: apply Hj'.
    unfold h in |- *; apply H; auto.
   apply om_fun_1; auto.
  exfalso; auto with zarith.
 exists (m + S n). exists (lt_n_Sn (m + S n)).
 elim le_lt_eq_dec; simpl in |- *; intro.
  exfalso; auto with zarith.
 apply H. inversion b0. auto.
Qed.

Lemma om_fun_3b : forall n m f g Hfg, nat_less_n_fun f -> nat_less_n_fun g ->
 forall i Hi, {j : nat | {Hj : j < m + n | g i Hi [=] om_fun n m f g Hfg j Hj}}.
Proof.
 intro n. induction  n as [| n Hrecn].
 simpl in |- *; intros. exists i.
  assert (i < m + 0). rewrite <- plus_n_O. auto.
   exists H1. algebra.
  intro m; induction  m as [| m Hrecm].
  simpl in |- *; intros. exfalso; inversion Hi.
  intros.
 simpl in |- *; elim ap_imp_less; simpl in |- *; intro.
  elim (le_lt_eq_dec _ _ Hi); intro.
   set (h := fun i Hi => g i (lt_S _ _ Hi)) in *.
   set (Hfh := fun i j Hi Hj => Hfg i j Hi (lt_S _ _ Hj)) in *.
   assert (Hh : nat_less_n_fun h). red in |- *; unfold h in |- *; auto.
    elim (Hrecm f h Hfh H Hh i (om_fun_lt _ _ a0)); intros j Hj.
   elim Hj; clear Hj; intros Hj Hj'.
   exists j; exists (lt_S _ _ Hj).
   elim le_lt_eq_dec; simpl in |- *; intro.
    eapply eq_transitive_unfolded. eapply eq_transitive_unfolded. 2: apply Hj'.
     unfold h in |- *; apply H0; auto.
    refine (om_fun_1 _ _ f h Hfh H Hh j j _ Hj (om_fun_lt _ _ a1)). auto.
    exfalso; auto with zarith.
  exists (m + S n). exists (lt_n_Sn (m + S n)).
  elim le_lt_eq_dec; simpl in |- *; intro.
   exfalso; auto with zarith.
  apply H0. inversion b. auto.
  set (h := fun i Hi => f i (lt_S _ _ Hi)) in *.
 set (Hfh := fun i j Hi Hj => Hfg i j (lt_S _ _ Hi) Hj) in *.
 assert (Hh : nat_less_n_fun h). red in |- *; unfold h in |- *; auto.
  elim (Hrecn _ h g Hfh Hh H0 i Hi); intros j Hj.
 elim Hj; clear Hj; intros Hj Hj'.
 cut (j < S (m + S n)). intro. 2: auto with zarith.
  exists j; exists H1.
 elim le_lt_eq_dec; simpl in |- *; intro.
  eapply eq_transitive_unfolded. apply Hj'. apply om_fun_1; auto.
   exfalso; auto with zarith.
Qed.

Lemma om_fun_4a : forall n m f g Hfg (P : F -> CProp), pred_wd F P ->
 (forall i Hi, P (f i Hi)) -> (forall j Hj, P (g j Hj)) -> forall k Hk, P (om_fun n m f g Hfg k Hk).
Proof.
 intro n. induction  n as [| n Hrecn].
 simpl in |- *; auto.
 intro m; induction  m as [| m Hrecm].
  simpl in |- *; auto.
 intros.
 simpl in |- *; elim ap_imp_less; simpl in |- *; intro; elim le_lt_eq_dec; simpl in |- *; intro; auto.
  set (h := fun i Hi => g i (lt_S _ _ Hi)) in *.
  set (Hfh := fun i j Hi Hj => Hfg i j Hi (lt_S _ _ Hj)) in *.
  set (Hh := fun i Hi => X1 i (lt_S _ _ Hi)) in *.
  exact (Hrecm f h Hfh P X X0 Hh k (om_fun_lt _ _ a0)).
 apply Hrecn; auto.
Qed.

Lemma om_fun_4b : forall n m f g Hfg (P : F -> Prop), pred_wd' F P ->
 (forall i Hi, P (f i Hi)) -> (forall j Hj, P (g j Hj)) -> forall k Hk, P (om_fun n m f g Hfg k Hk).
Proof.
 intro n. induction  n as [| n Hrecn].
 simpl in |- *; auto.
 intro m; induction  m as [| m Hrecm].
  simpl in |- *; auto.
 intros.
 simpl in |- *; elim ap_imp_less; simpl in |- *; intro; elim le_lt_eq_dec; simpl in |- *; intro; auto.
  set (h := fun i Hi => g i (lt_S _ _ Hi)) in *.
  set (Hfh := fun i j Hi Hj => Hfg i j Hi (lt_S _ _ Hj)) in *.
  set (Hh := fun i Hi => H1 i (lt_S _ _ Hi)) in *.
  exact (Hrecm f h Hfh P H H0 Hh k (om_fun_lt _ _ a0)).
 apply Hrecn; auto.
Qed.

Lemma om_fun_4c : forall n m f g Hfg (P : F -> CProp), pred_wd F P ->
 nat_less_n_fun f -> nat_less_n_fun g ->
 {i : nat | {Hi : i < n | P (f i Hi)}} or {j : nat | {Hj : j < m | P (g j Hj)}} ->
 {k : nat | {Hk : k < m + n | P (om_fun n m f g Hfg k Hk)}}.
Proof.
 intros n m f g Hfg P HP Hf Hg H.
 elim H; intro H'; elim H'; intros i Hi; elim Hi; clear H H' Hi; intros Hi Hi'.
  elim (om_fun_3a _ _ _ _ Hfg Hf Hg i Hi). intros j Hj. elim Hj; clear Hj.
  intros Hj Hj'.
  exists j; exists Hj; apply HP with (x := f i Hi); auto.
 elim (om_fun_3b _ _ _ _ Hfg Hf Hg i Hi). intros j Hj. elim Hj; clear Hj.
 intros Hj Hj'.
 exists j; exists Hj; apply HP with (x := g i Hi); auto.
Qed.

Lemma om_fun_4d : forall n m f g Hfg (P : F -> Prop), pred_wd' F P ->
 nat_less_n_fun f -> nat_less_n_fun g ->
 {i : nat | {Hi : i < n | P (f i Hi)}} or {j : nat | {Hj : j < m | P (g j Hj)}} ->
 {k : nat | {Hk : k < m + n | P (om_fun n m f g Hfg k Hk)}}.
Proof.
 intros n m f g Hfg P HP Hf Hg H.
 elim H; intro H'; elim H'; intros i Hi; elim Hi; clear H H' Hi; intros Hi Hi'.
  elim (om_fun_3a _ _ _ _ Hfg Hf Hg i Hi). intros j Hj. elim Hj; clear Hj.
  intros Hj Hj'.
  exists j; exists Hj; apply HP with (x := f i Hi); auto.
 elim (om_fun_3b _ _ _ _ Hfg Hf Hg i Hi). intros j Hj. elim Hj; clear Hj.
 intros Hj Hj'.
 exists j; exists Hj; apply HP with (x := g i Hi); auto.
Qed.

(* begin hide *)
Variable f : nat -> nat.
Hypothesis f0 : f 0 = 0.
Hypothesis f_mon : forall i j : nat, i < j -> f i < f j.

Variable h : nat -> F.
(* end hide *)

(**
** Summations
Also, some technical stuff on sums.  The first lemma relates two
different kinds of sums; the other two ones are variations, where the
structure of the arguments is analyzed in more detail.
*)

Lemma Sumx_Sum_Sum
 : forall n,
 Sumx (fun i (H : i < n) => Sum (f i) (pred (f (S i))) h) [=]
   Sumx (fun i (H : i < f n) => h i).
Proof.
 simple induction n.
  rewrite f0; simpl in |- *; algebra.
 clear n; intros.
 elim (le_lt_dec n 0); intro.
  cut (n = 0); [ clear a; intro | auto with arith ].
  rewrite H0 in H. rewrite H0. clear H0.
  simpl in |- *. astepl (Sum (f 0) (pred (f 1)) h). rewrite f0.
  apply eq_symmetric. eapply eq_transitive.
  apply Sumx_to_Sum.
    pattern 0 at 1 in |- *; rewrite <- f0; apply f_mon; apply lt_n_Sn.
   intros i j H0 H1 H'; rewrite H0; algebra.
  clear H; apply Sum_wd'; unfold part_tot_nat_fun in |- *; auto with arith.
  intros. elim (le_lt_dec (f 1) i); intro; simpl in |- *.
  cut (0 < f 1).
    intro; exfalso; lia.
   pattern 0 at 1 in |- *; rewrite <- f0; apply f_mon; apply lt_n_Sn.
  algebra.
 cut (0 < f n); [ intro | rewrite <- f0; apply f_mon; assumption ].
 simpl in |- *.
 eapply eq_transitive_unfolded.
  2: apply eq_symmetric_unfolded; apply Sumx_to_Sum.
   apply eq_transitive_unfolded with (Sum 0 (pred (f n))
     (part_tot_nat_fun _ _ (fun (i : nat) (H : i < f n) => h i)) [+] Sum (f n) (pred (f (S n))) h).
    apply bin_op_wd_unfolded.
     eapply eq_transitive_unfolded.
      apply H.
     apply Sumx_to_Sum; try assumption.
     red in |- *; intros; rewrite H1; algebra.
    algebra.
   cut (f n = S (pred (f n))); [ intro | apply S_pred with 0; auto ].
   setoid_rewrite H1 at 3.
   eapply eq_transitive_unfolded.
    2: apply Sum_Sum with (m := pred (f n)).
   apply bin_op_wd_unfolded; apply Sum_wd'.
      rewrite <- H1; apply lt_le_weak; assumption.
     intros.
     elim (le_lt_dec (f n) i); intro; simpl in |- *.
      exfalso; lia.
     elim (le_lt_dec (f (S n)) i); intro; simpl in |- *.
      cut (f n < f (S n)); [ intro | apply f_mon; apply lt_n_Sn ].
      exfalso; apply (le_not_lt (f n) i); auto.
      apply le_trans with (f (S n)); auto with arith.
     intros; unfold part_tot_nat_fun in |- *;
       elim (le_lt_dec (f (S n)) i);elim (le_lt_dec (f n) i);simpl;intros; try reflexivity;try exfalso; try lia.
    rewrite <-H1; cut (0 < f (S n)); [ intro | rewrite <- f0; auto with arith ];
      cut (f (S n) = S (pred (f (S n)))); [ intro | apply S_pred with 0; auto ];
        rewrite <- H3; apply lt_le_weak; auto with arith.
   intros; unfold part_tot_nat_fun in |- *;elim (le_lt_dec (f (S n)) i);
     [intro; simpl in |- *; exfalso; lia| reflexivity].
  apply lt_trans with (f n); auto with arith.
 red in |- *; intros; rewrite -> H1; reflexivity.
Qed.

Lemma str_Sumx_Sum_Sum :
 forall n (g : (forall i Hi, nat -> F)),
 (forall i j Hi, f i <= j -> j < f (S i) -> g i Hi j [=] h j) ->
 forall m, m = f n ->
 Sumx (fun i (H : i < n) => Sum (f i) (pred (f (S i))) (g i H)) [=]
 Sumx (fun i (H : i < m) => h i).
Proof.
 intros.
 rewrite H0.
 eapply eq_transitive_unfolded.
  2: apply Sumx_Sum_Sum.
 apply Sumx_wd.
 intros.
 apply Sum_wd'.
  cut (0 < f (S i)); [ intro | rewrite <- f0; auto with arith ].
  cut (f (S i) = S (pred (f (S i)))); [ intro | apply S_pred with 0; auto ].
  rewrite <- H3.
  apply lt_le_weak; auto with arith.
 intros; apply H.
  assumption.
 rewrite (S_pred (f (S i)) 0); auto with arith.
 rewrite <- f0; auto with arith.
Qed.

End Lemmas.

Section More_Lemmas.
(* begin hide *)
Let f' (m : nat) (f : forall i, i <= m -> nat) : nat -> nat.
Proof.
 intros i.
 elim (le_lt_dec i m); intro.
  apply (f i a).
 apply (f m (le_n m) + i).
Defined.
(* end hide *)

Variable F : COrdField.

Lemma str_Sumx_Sum_Sum' :
 forall (m : nat) (f : forall i, i <= m -> nat),
 f 0 (le_O_n _) = 0 ->
 (forall (i j : nat) Hi Hj, i = j -> f i Hi = f j Hj) ->
 (forall (i j : nat) Hi Hj, i < j -> f i Hi < f j Hj) ->
 forall (h : nat -> F) (n : nat) (g : forall i : nat, i < m -> nat -> F),
 (forall (i j : nat) Hi Hi' Hi'',
  f i Hi' <= j -> j < f (S i) Hi'' -> g i Hi j [=] h j) ->
 (forall H, n = f m H) ->
 Sumx
   (fun (i : nat) (H : i < m) =>
    Sum (f i (lt_le_weak _ _ H)) (pred (f (S i) H)) (g i H)) [=]
 Sumx (fun (i : nat) (_ : i < n) => h i).
Proof.
 intros.
 cut (forall (i : nat) (H : i <= m), f i H = f' m f i).
  intros.
  apply eq_transitive_unfolded with (Sumx (fun (i : nat) (H3 : i < m) =>
    Sum (f' m f i) (pred (f' m f (S i))) (g i H3))).
   apply Sumx_wd; intros.
   rewrite <- (H4 i (lt_le_weak _ _ H5)); rewrite <- (H4 (S i) H5); apply Sum_wd'.
    rewrite <- (S_pred (f (S i) H5) (f i (lt_le_weak _ _ H5)) (H1 _ _ _ _ (lt_n_Sn i))) .
    apply lt_le_weak; apply H1; apply lt_n_Sn.
   intros; algebra.
  apply str_Sumx_Sum_Sum.
     unfold f' in |- *; simpl in |- *.
     elim (le_lt_dec 0 m); intro; simpl in |- *.
      transitivity (f 0 (le_O_n m)).
       apply H0; auto.
      apply H.
     exfalso; inversion b.
    intros; apply nat_local_mon_imp_mon.
     clear H5 j i; intros.
     unfold f' in |- *.
     elim (le_lt_dec i m); elim (le_lt_dec (S i) m); intros; simpl in |- *.
        apply H1; apply lt_n_Sn.
       cut (i = m); [ intro | apply le_antisym; auto with arith ].
       generalize a; clear a; pattern i at 1 2 in |- *; rewrite H5; intro.
       set (x := f m a) in *.
       cut (x = f m (le_n m)).
        2: unfold x in |- *; apply H0; auto.
       intro.
       rewrite <- H6.
       rewrite <- plus_n_Sm; auto with arith.
      exfalso; apply (le_not_lt i m); auto with arith.
     set (x := f m (le_n m)) in *; clearbody x; auto with arith.
    assumption.
   intros.
   apply H2 with (Hi' := lt_le_weak _ _ Hi) (Hi'' := Hi).
    rewrite H4; assumption.
   rewrite H4; assumption.
  unfold f' in |- *.
  elim (le_lt_dec m m); intro; simpl in |- *.
   apply H3.
  elim (lt_irrefl _ b).
 clear H3 H2 g n h; intros.
 unfold f' in |- *.
 elim (le_lt_dec i m); intro; simpl in |- *.
  apply H0; auto.
 elim (le_not_lt i m); auto.
Qed.

End More_Lemmas.

author: coq-community

repo: corn

save_path: github-repos/coq/coq-community-corn


text:
From Coq Require Import MSetInterface MSetList MSetAVL MSetFacts MSetProperties MSetDecide.
From MetaCoq.Lob.Template.QuoteGround Require Export Coq.Numbers Coq.Init Coq.Lists.

Module QuoteWSetsOn (E : DecidableType) (Import W : WSetsOn E).
  Module WFacts := WFactsOn E W.
  Module WProperties := WPropertiesOn E W.
  Module WDecide := WDecideOn E W.

  Module Definitions.
    Section with_quote.
      Context {qelt : quotation_of elt} {qt : quotation_of t}
              {qIn : quotation_of In}
              {qeq_dec : quotation_of eq_dec}
              {qsubset_spec : quotation_of subset_spec}
              {qempty : quotation_of empty}
              {qadd : quotation_of add} {qelements : quotation_of elements}.

      #[export] Instance qEqual : quotation_of Equal := ltac:(cbv [Equal]; exact _).
      #[export] Instance qSubset : quotation_of Subset := ltac:(cbv [Subset]; exact _).
      #[export] Instance qEmpty : quotation_of Empty := ltac:(cbv [Empty]; exact _).

      #[export] Instance quote_In {x y} {qx : quotation_of x} {qy : quotation_of y} : ground_quotable (In x y)
        := ground_quotable_of_dec (WProperties.In_dec x y).
      #[export] Instance quote_neg_In {x y} {qx : quotation_of x} {qy : quotation_of y} : ground_quotable (~In x y)
        := ground_quotable_neg_of_dec (WProperties.In_dec x y).
      #[export] Instance quote_Equal {x y} {qx : quotation_of x} {qy : quotation_of y}  : ground_quotable (Equal x y)
        := ground_quotable_of_dec (eq_dec x y).
      #[export] Instance quote_neg_Equal {x y} {qx : quotation_of x} {qy : quotation_of y} : ground_quotable (~Equal x y)
        := ground_quotable_neg_of_dec (eq_dec x y).
      #[export] Instance quote_Subset {x y} {qx : quotation_of x} {qy : quotation_of y} : ground_quotable (Subset x y) := ground_quotable_of_iff (@subset_spec x y).
      #[export] Instance quote_neg_Subset {x y} {qx : quotation_of x} {qy : quotation_of y} : ground_quotable (~Subset x y) := quote_neg_of_iff (@subset_spec x y).
      #[export] Instance quote_Empty {x} {qx : quotation_of x} : ground_quotable (Empty x) := ground_quotable_of_iff (conj (@WProperties.empty_is_empty_2 x) (@WProperties.empty_is_empty_1 x)).
      #[export] Instance quote_neg_Empty {x} {qx : quotation_of x} : ground_quotable (~Empty x) := quote_neg_of_iff (conj (@WProperties.empty_is_empty_2 x) (@WProperties.empty_is_empty_1 x)).
      #[export] Instance quote_Add {x s s'} {qx : quotation_of x} {qs : quotation_of s} {qs' : quotation_of s'} : ground_quotable (WProperties.Add x s s')
        := ground_quotable_of_iff (iff_sym (WProperties.Add_Equal _ _ _)).
      #[export] Instance quote_neg_Add {x s s'} {qx : quotation_of x} {qs : quotation_of s} {qs' : quotation_of s'} : ground_quotable (~WProperties.Add x s s')
        := quote_neg_of_iff (iff_sym (WProperties.Add_Equal _ _ _)).

      Definition For_all_alt (P : elt -> Prop) (s : t) : Prop
        := List.Forall P (elements s).
      #[local] Hint Extern 1 (E.eq _ _) => reflexivity : core.
      Lemma For_all_alt_iff {P} {P_Proper : Proper (E.eq ==> Basics.impl) P} {s}
        : For_all_alt P s <-> For_all P s.
      Proof using Type.
        cbv [For_all_alt For_all].
        setoid_rewrite WFacts.elements_iff.
        induction (elements s) as [|x xs IH].
        { split; solve [ constructor | inversion 2 ]. }
        { setoid_rewrite Forall_cons_iff; setoid_rewrite InA_cons; setoid_rewrite IH.
          intuition auto.
          eapply P_Proper; (idtac + symmetry); eassumption. }
      Defined.
      #[export] Instance qFor_all : quotation_of For_all := ltac:(cbv [For_all]; exact _).
      #[export] Instance qExists : quotation_of Exists := ltac:(cbv [Exists]; exact _).
      Definition quote_For_all {P s} {quote_elt : ground_quotable elt} {quote_P : forall x, ground_quotable (P x:Prop)} {qP : quotation_of P} {P_Proper : Proper (E.eq ==> Basics.impl) P} {qP_Proper : quotation_of P_Proper} {qs : quotation_of s} : ground_quotable (For_all P s)
        := ground_quotable_of_iff For_all_alt_iff.
      Lemma For_all_forall_iff {P s} : (For_all P s) <-> (forall v, In v s -> P v).
      Proof using Type. reflexivity. Qed.
      Lemma For_all_forall2_iff {P s} : (For_all (fun v1 => For_all (P v1) s) s) <-> (forall v1 v2, In v1 s -> In v2 s -> P v1 v2).
      Proof using Type. cbv [For_all]; intuition eauto. Qed.
      #[export] Instance quote_forall2_In {P s} {qP : quotation_of P} {qs : quotation_of s} {quote_For_all : ground_quotable (For_all (fun v1 => For_all (P v1) s) s)} : ground_quotable (forall v1 v2, In v1 s -> In v2 s -> P v1 v2)
        := ground_quotable_of_iff For_all_forall2_iff.

      Definition Exists_alt (P : elt -> Prop) (s : t) : Prop
        := List.Exists P (elements s).
      Lemma Exists_alt_iff {P} {P_Proper : Proper (E.eq ==> Basics.impl) P} {s}
        : Exists_alt P s <-> Exists P s.
      Proof.
        cbv [Exists_alt Exists].
        setoid_rewrite WFacts.elements_iff.
        induction (elements s) as [|x xs IH].
        { split; try solve [ constructor | inversion 1 | intros [x [H H']]; inversion H ]. }
        { setoid_rewrite Exists_cons; setoid_rewrite InA_cons; setoid_rewrite IH.
          firstorder intuition auto. }
      Defined.
      Definition Exists_dec {P s} (P_dec : forall x, {P x} + {~P x}) {P_Proper : Proper (E.eq ==> Basics.impl) P} : {Exists P s} + {~Exists P s}.
      Proof.
        destruct (List.Exists_dec P (elements s) P_dec) as [H|H]; [ left | right ]; revert H.
        { intro H; apply Exists_alt_iff, H. }
        { intros H H'; apply H, Exists_alt_iff, H'. }
      Defined.

      Definition quote_Exists_dec {P} (P_dec : forall x, {P x} + {~P x}) {s} {quote_elt : ground_quotable elt} {qP_dec : quotation_of P_dec} {quote_P : forall x, ground_quotable (P x:Prop)} {qP : quotation_of P} {P_Proper : Proper (E.eq ==> Basics.impl) P} {qP_Proper : quotation_of P_Proper} {qs : quotation_of s} : ground_quotable (Exists P s)
        := ground_quotable_of_dec (Exists_dec P_dec).
    End with_quote.
  End Definitions.

  Include Definitions.

  Module Export Instances.
    #[export] Existing Instances
     quote_In
     quote_Equal
     quote_Subset
     quote_Empty
     quote_Add
     quote_neg_In
     quote_neg_Equal
     quote_neg_Subset
     quote_neg_Empty
     quote_neg_Add
     quote_forall2_In
    .
    #[export] Hint Extern 9 (ground_quotable (For_all _ _))
    => simple notypeclasses refine (@quote_For_all _ _ _ _ _ _ _ _ _ _ _) : typeclass_instances.
  End Instances.
End QuoteWSetsOn.

Module QuoteSetsOn (E : OrderedType) (Import M : SetsOn E).
  Include QuoteWSetsOn E M.
  Module Import MOrdProperties. Module E := E. Include M <+ OrdProperties. End MOrdProperties.

  Module OnlyOrdDefinitions.
    Definition above x s : bool := for_all (fun y => if ME.lt_dec y x then true else false) s.
    Definition below x s : bool := for_all (fun y => if ME.lt_dec x y then true else false) s.
    Lemma above_spec x s : above x s = true <-> Above x s.
    Proof.
      cbv [Above above].
      rewrite for_all_spec
        by (intros ?? H; repeat (let H' := fresh in destruct ME.lt_dec as [H'|H']; rewrite ?H in H'); try reflexivity; tauto).
      cbv [For_all].
      split; intros H y H'; generalize (H y H'); destruct ME.lt_dec; try reflexivity; eauto; congruence.
    Qed.
    Lemma below_spec x s : below x s = true <-> Below x s.
    Proof.
      cbv [Below below].
      rewrite for_all_spec
        by (intros ?? H; repeat (let H' := fresh in destruct ME.lt_dec as [H'|H']; rewrite ?H in H'); try reflexivity; tauto).
      cbv [For_all].
      split; intros H y H'; generalize (H y H'); destruct ME.lt_dec; try reflexivity; eauto; congruence.
    Qed.
    #[export] Instance quote_Above {x s} {qx : quotation_of x} {qs : quotation_of s} : ground_quotable (Above x s)
      := ground_quotable_of_iff (above_spec x s).
    #[export] Instance quote_Below {x s} {qx : quotation_of x} {qs : quotation_of s} : ground_quotable (Below x s)
      := ground_quotable_of_iff (below_spec x s).
  End OnlyOrdDefinitions.

  Module OrdDefinitions.
    Include Definitions.
    Include OnlyOrdDefinitions.
  End OrdDefinitions.

  Include OnlyOrdDefinitions.

  Module Export OnlyOrdInstances.
    #[export] Existing Instances
     quote_Above
     quote_Below
    .
  End OnlyOrdInstances.
  Module Export OrdInstances.
    Export Instances.
    Export OnlyOrdInstances.
  End OrdInstances.
End QuoteSetsOn.

Module Type MSetAVL_MakeSig (T : OrderedType). Include MSetAVL.Make T. End MSetAVL_MakeSig.

Module QuoteMSetAVL (T : OrderedType) (M : MSetAVL_MakeSig T).
  Module Import QM := QuoteSetsOn T M.

  Module Definitions.
    Include QM.OrdDefinitions.

    Scheme Induction for M.Raw.tree Sort Type.
    Scheme Induction for M.Raw.tree Sort Set.
    Scheme Induction for M.Raw.tree Sort Prop.
    Scheme Case for M.Raw.tree Sort Type.
    Scheme Case for M.Raw.tree Sort Prop.
    Scheme Minimality for M.Raw.tree Sort Type.
    Scheme Minimality for M.Raw.tree Sort Set.
    Scheme Minimality for M.Raw.tree Sort Prop.

    Section with_t.
      Context {quote_T_t : ground_quotable T.t}
              {qRaw_tree : inductive_quotation_of M.Raw.tree}
              {qRaw_bst : inductive_quotation_of M.Raw.bst}
              {qt_ : inductive_quotation_of M.t_}.

      #[export] Instance quote_M_Raw_t : ground_quotable M.Raw.t := (ltac:(induction 1; exact _)).
      Fixpoint M_Raw_lt_tree_dec x t : { M.Raw.lt_tree x t } + {~ M.Raw.lt_tree x t}.
      Proof.
        refine match t with
               | M.Raw.Leaf => left _
               | M.Raw.Node z l n r
                 => match T.compare n x as c, M_Raw_lt_tree_dec x l, M_Raw_lt_tree_dec x r return CompareSpec _ _ _ c -> _ with
                    | Lt, left p2, left p3 => fun pfc => left _
                    | _, right pf, _ => fun pfc => right _
                    | _, _, right pf => fun pfc => right _
                    | _, _, _ => fun pfc => right _
                    end (T.compare_spec _ _)
               end;
          try solve [ inversion 1; inversion pfc
                    | inversion 1; inversion pfc; subst; auto;
                      match goal with
                      | [ H : T.lt _ _, H' : T.eq _ _ |- _ ]
                        => now first [ rewrite -> H' in H | rewrite <- H' in H ]
                      end
                    | intro f; apply pf; hnf in *; intros; apply f; constructor; (assumption + reflexivity)
                    | intro f; inversion pfc; eapply M.Raw.MX.lt_irrefl; (idtac + etransitivity); (eassumption + (eapply f; constructor; (idtac + symmetry); (eassumption + reflexivity))) ].
      Defined.
      Fixpoint M_Raw_gt_tree_dec x t : { M.Raw.gt_tree x t } + {~ M.Raw.gt_tree x t}.
      Proof.
        refine match t with
               | M.Raw.Leaf => left _
               | M.Raw.Node z l n r
                 => match T.compare n x as c, M_Raw_gt_tree_dec x l, M_Raw_gt_tree_dec x r return CompareSpec _ _ _ c -> _ with
                    | Gt, left p2, left p3 => fun pfc => left _
                    | _, right pf, _ => fun pfc => right _
                    | _, _, right pf => fun pfc => right _
                    | _, _, _ => fun pfc => right _
                    end (T.compare_spec _ _)
               end;
          try solve [ inversion 1; inversion pfc
                    | inversion 1; inversion pfc; subst; auto;
                      match goal with
                      | [ H : T.lt _ _, H' : T.eq _ _ |- _ ]
                        => now first [ rewrite -> H' in H | rewrite <- H' in H ]
                      end
                    | intro f; apply pf; hnf in *; intros; apply f; constructor; (assumption + reflexivity)
                    | intro f; inversion pfc; eapply M.Raw.MX.lt_irrefl; (idtac + etransitivity); (eassumption + (eapply f; constructor; (idtac + symmetry); (eassumption + reflexivity))) ].
      Defined.
      Fixpoint M_Raw_bst_dec t : { M.Raw.bst t } + {~ M.Raw.bst t}.
      Proof.
        refine match t with
               | M.Raw.Leaf => left _
               | M.Raw.Node z l n r
                 => match M_Raw_bst_dec l, M_Raw_bst_dec r, M_Raw_lt_tree_dec n l, M_Raw_gt_tree_dec n r with
                    | right pf, _, _, _ => right _
                    | _, right pf, _, _ => right _
                    | _, _, right pf, _ => right _
                    | _, _, _, right pf => right _
                    | left p1, left p2, left p3, left p4 => left _
                    end
               end;
          try solve [ constructor; assumption
                    | inversion 1; subst; auto ].
      Defined.
      #[export] Instance quote_Raw_bst t : ground_quotable (M.Raw.bst t)
        := ground_quotable_of_dec (@M_Raw_bst_dec t).
      #[export] Instance quote_Raw_Ok s : ground_quotable (M.Raw.Ok s) := (ltac:(cbv [M.Raw.Ok]; exact _)).
      #[export] Instance quote_t : ground_quotable M.t := ltac:(induction 1; exact _).
    End with_t.
  End Definitions.
  Include Definitions.
  Module Export Instances.
    Export QM.OrdInstances.
    #[export] Existing Instances
     quote_M_Raw_t
     quote_Raw_bst
     quote_Raw_Ok
     quote_t
    .
  End Instances.
End QuoteMSetAVL.

Module QuoteUsualWSetsOn (E : UsualDecidableType) (Import M : WSetsOn E).
  Module Import QM := QuoteWSetsOn E M.

  Module Definitions.
    Notation quote_In := QM.quote_In.
    Notation quote_Equal := QM.quote_Equal.
    Notation quote_Subset := QM.quote_Subset.
    Notation quote_Empty := QM.quote_Empty.
    Notation quote_Add := QM.quote_Add.
    Notation quote_neg_In := QM.quote_neg_In.
    Notation quote_neg_Equal := QM.quote_neg_Equal.
    Notation quote_neg_Subset := QM.quote_neg_Subset.
    Notation quote_neg_Empty := QM.quote_neg_Empty.
    Notation quote_neg_Add := QM.quote_neg_Add.

    Section with_quote.
      Context {qelt : quotation_of elt} {qt : quotation_of t}
              {qIn : quotation_of In}
              {qeq_dec : quotation_of eq_dec}
              {qsubset_spec : quotation_of subset_spec}
              {qempty : quotation_of empty}
              {qadd : quotation_of add} {qelements : quotation_of elements}.

      #[export] Instance quote_For_all {P s} {quote_elt : ground_quotable elt} {quote_P : forall x, ground_quotable (P x:Prop)} {qP : quotation_of P} {qs : quotation_of s} : ground_quotable (For_all P s)
        := QM.quote_For_all.
      Definition quote_Exists_dec {P} (P_dec : forall x, {P x} + {~P x}) {s} {quote_elt : ground_quotable elt} {qP_dec : quotation_of P_dec} {quote_P : forall x, ground_quotable (P x:Prop)} {qP : quotation_of P} {qs : quotation_of s} : ground_quotable (Exists P s)
        := QM.quote_Exists_dec P_dec.
      #[export] Instance quote_forall2_In {P s} {qP : quotation_of P} {qs : quotation_of s} {quote_elt : ground_quotable elt} {quote_P : forall x y, ground_quotable (P x y:Prop)} : ground_quotable (forall v1 v2, In v1 s -> In v2 s -> P v1 v2) := _.
    End with_quote.
  End Definitions.

  Include Definitions.

  Module Export Instances.
    #[export] Existing Instances
     QM.quote_In
     QM.quote_Equal
     QM.quote_Subset
     QM.quote_Empty
     QM.quote_Add
     QM.quote_neg_In
     QM.quote_neg_Equal
     QM.quote_neg_Subset
     QM.quote_neg_Empty
     QM.quote_neg_Add
     quote_For_all
     quote_forall2_In
    .
  End Instances.
End QuoteUsualWSetsOn.

Module QuoteUsualSetsOn (E : UsualOrderedType) (Import M : SetsOn E).
  Module QM := QuoteUsualWSetsOn E M.
  Module QM' := QuoteSetsOn E M.

  Module Definitions := QM.Definitions <+ QM'.OnlyOrdDefinitions.
  Include Definitions.

  Module Export Instances := QM.Instances <+ QM'.OnlyOrdInstances.
End QuoteUsualSetsOn.

Module QuoteSetsOnWithLeibniz (E : OrderedTypeWithLeibniz) (Import M : SetsOn E).
  Module Import QM := QuoteSetsOn E M.

  Module Definitions.
    Notation quote_In := QM.quote_In.
    Notation quote_Equal := QM.quote_Equal.
    Notation quote_Subset := QM.quote_Subset.
    Notation quote_Empty := QM.quote_Empty.
    Notation quote_Add := QM.quote_Add.
    Notation quote_neg_In := QM.quote_neg_In.
    Notation quote_neg_Equal := QM.quote_neg_Equal.
    Notation quote_neg_Subset := QM.quote_neg_Subset.
    Notation quote_neg_Empty := QM.quote_neg_Empty.
    Notation quote_neg_Add := QM.quote_neg_Add.
    Notation quote_Above := QM.quote_Above.
    Notation quote_Below := QM.quote_Below.

    #[local] Instance all_P_Proper {P : E.t -> Prop} : Proper (E.eq ==> Basics.impl) P.
    Proof.
      intros ?? H.
      apply E.eq_leibniz in H; subst; exact id.
    Defined.

    Section with_quote.
      Context {qelt : quotation_of elt} {qt : quotation_of t}
              {qIn : quotation_of In}
              {qeq_dec : quotation_of eq_dec}
              {qsubset_spec : quotation_of subset_spec}
              {qempty : quotation_of empty}
              {qadd : quotation_of add} {qelements : quotation_of elements}.

      #[export] Instance quote_For_all {P s} {quote_elt : ground_quotable elt} {quote_P : forall x, ground_quotable (P x:Prop)} {qP : quotation_of P} {qs : quotation_of s} : ground_quotable (For_all P s)
        := QM.quote_For_all.
      Definition quote_Exists_dec {P} (P_dec : forall x, {P x} + {~P x}) {s} {quote_elt : ground_quotable elt} {qP_dec : quotation_of P_dec} {quote_P : forall x, ground_quotable (P x:Prop)} {qP : quotation_of P} {qs : quotation_of s} : ground_quotable (Exists P s)
        := QM.quote_Exists_dec P_dec.
      #[export] Instance quote_forall2_In {P s} {qP : quotation_of P} {qs : quotation_of s} {quote_elt : ground_quotable elt} {quote_P : forall x y, ground_quotable (P x y:Prop)} : ground_quotable (forall v1 v2, In v1 s -> In v2 s -> P v1 v2) := _.
    End with_quote.
  End Definitions.

  Include Definitions.

  Module Export Instances.
    #[export] Existing Instances
     QM.quote_In
     QM.quote_Equal
     QM.quote_Subset
     QM.quote_Empty
     QM.quote_Add
     QM.quote_neg_In
     QM.quote_neg_Equal
     QM.quote_neg_Subset
     QM.quote_neg_Empty
     QM.quote_neg_Add
     quote_For_all
     quote_forall2_In
     QM.quote_Above
     QM.quote_Below
    .
  End Instances.
End QuoteSetsOnWithLeibniz.

Module Type MSetList_MakeSig (T : OrderedType). Include MSetList.Make T. End MSetList_MakeSig.

Module QuoteMSetList (E : OrderedType) (Import M : MSetList_MakeSig E).
  Module Import QM := QuoteSetsOn E M.

  Module OnlyMSetListDefinitions.
    #[export] Instance quote_Ok {qE_compare : quotation_of E.compare} {qE_t : quotation_of E.t} {v} : ground_quotable (Raw.Ok v) := ltac:(cbv [Raw.Ok]; exact _).

    #[export] Instance quote_t_ {qE_t : quotation_of E.t} {qE_compare : quotation_of E.compare} {quoteE_t : ground_quotable E.t} {qM_Mkt : quotation_of M.Mkt} : ground_quotable t_ := ltac:(destruct 1; exact _).
  End OnlyMSetListDefinitions.

  Module Definitions := QM.Definitions <+ OnlyMSetListDefinitions.
  Include Definitions.

  Module OnlyMSetListInstances.
    #[export] Existing Instances
     quote_Ok
     quote_t_
    .
  End OnlyMSetListInstances.

  Module Export Instances := QM.Instances <+ OnlyMSetListInstances.
End QuoteMSetList.

Module QuoteMSetListWithLeibniz (E : OrderedTypeWithLeibniz) (Import M : MSetList_MakeSig E).
  Module QM := QuoteSetsOnWithLeibniz E M.
  Module QM' := QuoteMSetList E M.

  Module Definitions := QM.Definitions <+ QM'.OnlyMSetListDefinitions.
  Include Definitions.

  Module Export Instances := QM.Instances <+ QM'.OnlyMSetListInstances.
End QuoteMSetListWithLeibniz.

repo: metacoq-lob

save_path: github-repos/coq/JasonGross-metacoq-lob


text:
(* Order of imports: import proofmode after utils after robinson *)
From Undecidability.FOL Require Import FullSyntax.
From Undecidability.FOL.Arithmetics Require Import Signature FA Robinson.

From Undecidability.FOL.Incompleteness Require Import utils fol_utils.
From Undecidability.FOL.Proofmode Require Import Theories ProofMode.

Require Import Lia.
Require Import String.

Open Scope string_scope.

(** ** Q-decidability *)
Section Qdec.
  Existing Instance PA_preds_signature.
  Existing Instance PA_funcs_signature.

  Definition Qdec φ := forall (pei : peirce) ρ, (forall k, bounded_t 0 (ρ k)) -> Qeq ⊢ φ[ρ] \/ Qeq ⊢ ¬φ[ρ].

  Lemma subst_t_closed t ρ : (forall k, bounded_t 0 (ρ k)) -> bounded_t 0 t`[ρ].
  Proof.
    intros H. destruct (find_bounded_t t) as [n Hn].
    eapply subst_bounded_max_t; last eassumption.
    intros l _. apply H.
  Qed.
  Lemma subst_closed φ ρ : (forall k, bounded_t 0 (ρ k)) -> bounded 0 φ[ρ].
  Proof.
    intros H. destruct (find_bounded φ) as [n Hn].
    eapply subst_bounded_max; last eassumption.
    intros l _. apply H.
  Qed.

  Lemma Qdec_subst φ ρ : Qdec φ -> Qdec φ[ρ].
  Proof.
    intros H pei ρ' Hb. rewrite subst_comp. apply H.
    intros k. apply subst_t_closed, Hb.
  Qed.

  Lemma Qdec_iff φ ψ : Qeq ⊢I φ ↔ ψ -> Qdec φ -> Qdec ψ.
  Proof.
    intros H Hφ pei ρ Hρ. apply prv_intu_peirce in H.
    pose proof (subst_Weak ρ H) as Hiff. cbn in Hiff. change (List.map _ _) with Qeq in Hiff.
    destruct (Hφ pei ρ Hρ) as [H1|H1].
    - left. fapply Hiff. fapply H1.
    - right. fintros. fapply H1. fapply Hiff. ctx.
  Qed.
  Lemma Qdec_iff' φ ψ :
    (forall ρ, (forall k, bounded_t 0 (ρ k)) -> Qeq ⊢I φ[ρ] ↔ ψ[ρ]) ->
    Qdec φ -> Qdec ψ.
  Proof.
    intros H Hφ pei ρ Hρ.
    specialize (H _ Hρ). apply prv_intu_peirce in H.
    destruct (Hφ _ _ Hρ) as [H1|H1].
    - left. fapply H. fapply H1.
    - right. fintros. fapply H1. fapply H. ctx.
  Qed.

  Lemma Qdec_bot : Qdec ⊥.
  Proof.
    intros ρ Hb. right. fintros. ctx.
  Qed.

  Lemma Qdec_and φ ψ : Qdec φ -> Qdec ψ -> Qdec (φ ∧ ψ).
  Proof.
    intros Hφ Hψ pei ρ Hb. cbn.
    destruct (Hφ _ _ Hb) as [H1|H1], (Hψ _ _ Hb) as [H2|H2].
    2-4: right; fintros; fdestruct 0.
    - left. now fsplit.
    - fapply H2. ctx.
    - fapply H1. ctx.
    - fapply H1. ctx.
  Qed.

  Lemma Qdec_or φ ψ : Qdec φ -> Qdec ψ -> Qdec (φ ∨ ψ).
  Proof.
    intros Hφ Hψ ρ pei Hb. cbn.
    destruct (Hφ _ _ Hb) as [H1|H1], (Hψ _ _ Hb) as [H2|H2].
    1-3: left; now (fleft + fright).
    right. fintros "[H|H]".
    - fapply H1. ctx.
    - fapply H2. ctx.
  Qed.

  Lemma Qdec_impl φ ψ : Qdec φ -> Qdec ψ -> Qdec (φ → ψ).
  Proof.
    intros Hφ Hψ pei ρ Hb. cbn.
    destruct (Hφ _ _ Hb) as [H1|H1], (Hψ _ _ Hb) as [H2|H2].
    - left. fintros. fapply H2.
    - right. fintros. fapply H2. fapply 0. fapply H1.
    - left. fintros. fapply H2.
    - left. fintros. fexfalso. fapply H1. ctx.
  Qed.

  Lemma Qdec_eq t s : Qdec (t == s).
  Proof.
    intros pei ρ Hb. cbn.
    destruct (@closed_term_is_num _ t`[ρ]) as [k1 Hk1].
    { apply subst_t_closed, Hb. }
    destruct (@closed_term_is_num _ s`[ρ]) as [k2 Hk2].
    { apply subst_t_closed, Hb. }
    assert (k1 = k2 \/ k1 <> k2) as [->|Hk] by lia; [left|right].
    all: frewrite Hk1; frewrite Hk2.
    - fapply ax_refl.
    - clear Hk1. clear Hk2. revert Hk. induction k1 in k2 |-*; intros Hk.
      + destruct k2; first congruence. cbn.
        fapply ax_zero_succ.
      + cbn. destruct k2.
        * fintros. fapply (ax_zero_succ (num k1)). fapply ax_sym. ctx.
        * cbn. fintros. assert (H' : k1 <> k2) by congruence.
          specialize (IHk1 k2 H'). fapply IHk1.
          fapply ax_succ_inj. ctx.
  Qed.
  Lemma Qdec_le t s : Qdec (t ⧀= s).
  Proof.
    intros pei ρ Hb.
    destruct (@closed_term_is_num _ t`[ρ]) as [k1 Hk1].
    { apply subst_t_closed, Hb. }
    destruct (@closed_term_is_num _ s`[ρ]) as [k2 Hk2].
    { apply subst_t_closed, Hb. }
    rewrite PAle_subst.
    enough (Qeq ⊢ num k1 ⧀= num k2 \/ Qeq ⊢ ¬(num k1 ⧀= num k2)) as [H|H].
    { left. unfold PAle. frewrite Hk1. frewrite Hk2. apply H. }
    { right. unfold PAle. frewrite Hk1. frewrite Hk2. apply H. }
    clear Hk1 Hk2.
    induction k1 as [|k1 IH] in k2 |-*.
    - left. fexists (num k2).
      frewrite (ax_add_zero (num k2)). fapply ax_refl.
    - destruct k2 as [|k2].
      + right.
        fstart. fintros "[z H]". fapply (ax_zero_succ (num k1 ⊕ z)).
        frewrite <-(ax_add_rec z (num k1)). fapply "H".
      + destruct (IH k2) as [IH'|IH'].
        * left. fstart.
          fassert (num k1 ⧀= num k2) as "H"; first apply IH'.
          fdestruct "H" as "[z Hz]".
          fexists z. frewrite (ax_add_rec z (num k1)).
          fapply ax_succ_congr. fapply "Hz".
        * right. fstart. fintros "H". fapply IH'.
          fdestruct "H" as "[z Hz]".
          fexists z. fapply ax_succ_inj.
          frewrite <-(ax_add_rec z (num k1)). fapply "Hz".
  Qed.

  Section lemmas.
    Context `{pei : peirce}.

    Lemma Qsdec_le x y : bounded_t 0 x -> Qeq ⊢ ((x ⧀= y) ∨ (y ⧀= x)).
    Proof.
      intros Hx. destruct (closed_term_is_num Hx) as [k Hk].
      unfold PAle. frewrite Hk. clear Hk.
      induction k as [|k IH] in y |-*; fstart.
      - fleft. fexists y. frewrite (ax_add_zero y). fapply ax_refl.
      - fassert (ax_cases); first ctx.
        fdestruct ("H" y) as "[H|[y' H]]".
        + fright. fexists (σ (num k)).
          frewrite "H". frewrite (ax_add_zero (σ num k)).
          fapply ax_refl.
        + specialize (IH y').
          fdestruct IH.
          * fleft.
            fdestruct "H0". fexists x0. frewrite "H". frewrite "H0".
            fapply ax_sym. fapply ax_add_rec.
          * fright. custom_simpl.
            fdestruct "H0". fexists x0. frewrite "H". frewrite "H0".
            fapply ax_sym. fapply ax_add_rec.
    Qed.
    Lemma Q_eqdec t x : Qeq ⊢ x == (num t) ∨ ¬(x == num t).
    Proof.
      induction t in x |-*; fstart; fintros.
      - fassert (ax_cases); first ctx.
        fdestruct ("H" x).
        + fleft. frewrite "H".
          fapply ax_refl.
        + fright. fdestruct "H". frewrite "H".
          fintros. fapply (ax_zero_succ x0).
          fapply ax_sym. ctx.
      - fassert (ax_cases); first ctx.
        fdestruct ("H" x).
        + fright. frewrite "H".
          fapply ax_zero_succ.
        + fdestruct "H". frewrite "H".
          specialize (IHt x0).
          fdestruct IHt.
          * fleft. fapply ax_succ_congr. fapply "H0".
          * fright. fintros. fapply "H0".
            fapply ax_succ_inj. fapply "H1".
    Qed.

    Lemma PAle_zero_eq x : Qeq ⊢ x ⧀= zero → x == zero.
    Proof.
      fstart. fintros. unfold PAle. fdestruct "H".
      fassert ax_cases.
      { ctx. }
      unfold ax_cases.
      fdestruct ("H0" x).
      - fapply "H0".
      - fdestruct "H0".
        fexfalso. fapply (ax_zero_succ (x1 ⊕ x0)).
        frewrite <- (ax_add_rec x0 x1). frewrite <- "H0".
        fapply "H".
    Qed.
    Lemma PAle'_zero_eq x : Qeq ⊢ (x ⧀=' zero) → x == zero.
    Proof.
      fstart. fintros. unfold PAle'. fdestruct "H".
      fassert ax_cases as "C"; first ctx.
      fdestruct ("C" x0) as "[Hx'|[x' Hx']]".
      - frewrite <-(ax_add_zero x). frewrite <-"Hx'".
        frewrite <-"H". frewrite "Hx'". fapply ax_refl.
      - fexfalso. fapply (ax_zero_succ (x' ⊕ x)).
        frewrite <-(ax_add_rec x x'). frewrite <-"Hx'".
        fapply "H".
    Qed.

    Lemma add_zero_swap t x :
      Qeq ⊢ x ⊕ zero == num t → x == num t.
    Proof.
      fstart. induction t in x |-*; fintros.
      - fassert (ax_cases); first ctx.
        fdestruct ("H0" x).
        + ctx.
        + fdestruct "H0".
          fexfalso. fapply (ax_zero_succ (x0 ⊕ zero)).
          frewrite <- (ax_add_rec zero x0).
          frewrite <-"H0". fapply ax_sym. ctx.
      - fassert (ax_cases); first ctx.
        fdestruct ("H0" x).
        + fexfalso. fapply (ax_zero_succ (num t)).
          frewrite <-"H". frewrite "H0".
          frewrite (ax_add_zero zero).
          fapply ax_refl.
        + fdestruct "H0".
          frewrite "H0". fapply ax_succ_congr.
          specialize (IHt x0).
          fapply IHt. fapply ax_succ_inj.
          frewrite <-(ax_add_rec zero x0).
          frewrite <- "H0". fapply "H".
    Qed.

    Lemma add_rec_swap t x y:
      Qeq ⊢ x ⊕ σ y == σ num t → x ⊕ y == num t.
    Proof.
      induction t in x |-*; fstart; fintros "H".
      - fassert ax_cases as "C"; first ctx.
        fdestruct ("C" x) as "[Hx|[x' Hx']]".
        + frewrite "Hx". frewrite (ax_add_zero y).
          fapply ax_succ_inj. frewrite <-(ax_add_zero (σ y)).
          frewrite <-"H". frewrite "Hx". fapply ax_refl.
        + frewrite "Hx'". fassert ax_cases as "C"; first ctx.
          fdestruct ("C" x') as "[Hx''|[x'' Hx'']]".
          * fexfalso. fapply (ax_zero_succ y).
            fapply ax_succ_inj. frewrite <-"H".
            frewrite "Hx'". frewrite "Hx''".
            frewrite (ax_add_rec (σ y) zero). frewrite (ax_add_zero (σ y)).
            fapply ax_refl.
          * fexfalso. fapply (ax_zero_succ (x'' ⊕ σ y)).
            fapply ax_succ_inj. frewrite <-"H".
            frewrite "Hx'". frewrite "Hx''".
            frewrite (ax_add_rec (σ y) (σ x'')).
            frewrite (ax_add_rec (σ y) x''). fapply ax_refl.
      - fassert ax_cases as "C"; first ctx.
        fdestruct ("C" x) as "[Hx'|[x' Hx']]".
        + fapply ax_succ_inj. frewrite <-"H".
          frewrite "Hx'". frewrite (ax_add_zero y).
          frewrite (ax_add_zero (σ y)). fapply ax_refl.
        + frewrite "Hx'". frewrite (ax_add_rec y x').
          fapply ax_succ_congr.
          specialize (IHt x'). fapply IHt.
          fapply ax_succ_inj. frewrite <-(ax_add_rec (σ y) x').
          frewrite <-"Hx'". ctx.
    Qed.

    Lemma PAle_sigma_neq t x : Qeq ⊢ (x ⧀= σ(num t)) → ¬(x == σ(num t)) → x ⧀= num t.
    Proof.
      fstart. fintros. unfold PAle. fdestruct "H". custom_simpl.
      fassert (ax_cases); first ctx.
      fdestruct ("H1" x0).
      - fexfalso. fapply "H0".
        pose proof (add_zero_swap (S t) x). cbn in H.
        fapply H. frewrite <- "H1". fapply ax_sym.
        ctx.
      - fdestruct "H1". fexists x1. custom_simpl.
        fapply ax_sym. fapply add_rec_swap.
        frewrite <-"H1". fapply ax_sym. fapply "H".
    Qed.
    Lemma PAle'_sigma_neq t x : Qeq ⊢ (x ⧀=' σ(num t)) → ¬(x == σ(num t)) → x ⧀=' num t.
    Proof.
      fstart. fintros. unfold PAle'.
      fdestruct "H" as "[z Hz]".
      fassert ax_cases as "C"; first ctx.
      fdestruct ("C" z) as "[Hz'|[z' Hz']]".
      - fexfalso. fapply "H0". frewrite "Hz". frewrite "Hz'".
        fapply ax_sym. fapply ax_add_zero.
      - fexists z'. fapply ax_succ_inj.
        frewrite <-(ax_add_rec x z').
        frewrite <-"Hz'". ctx.
    Qed.

    Lemma add_rec_swap2 t x y :
      Qeq ⊢ x ⊕ y == num t → x ⊕ (σ y) == num (S t).
    Proof.
      induction t in x |-*; fstart; fintros "H".
      - fassert ax_cases as "C"; first ctx.
        fdestruct ("C" x) as "[Hx'|[x' Hx']]".
        + frewrite <-"H". frewrite "Hx'".
          frewrite (ax_add_zero (σ y)). frewrite (ax_add_zero y).
          fapply ax_refl.
        + fexfalso. fapply (ax_zero_succ (x' ⊕ y)). frewrite <-"H".
          frewrite "Hx'". frewrite (ax_add_rec y x'). fapply ax_refl.
      - fassert ax_cases as "C"; first ctx.
        fdestruct ("C" x) as "[Hx'|[x' Hx']]".
        + frewrite <-"H". frewrite "Hx'".
          frewrite (ax_add_zero (σ y)). frewrite (ax_add_zero y).
          fapply ax_refl.
        + frewrite "Hx'". frewrite (ax_add_rec (σ y) x').
          fapply ax_succ_congr.
          fapply IHt. fapply ax_succ_inj.
          frewrite <-(ax_add_rec y x'). frewrite <-"Hx'".
          fapply "H".
    Qed.

    Lemma PAle_succ t x : Qeq ⊢ (x ⧀= num t) → (x ⧀= σ (num t)).
    Proof.
      fstart. fintros "[z Hz]". fexists (σ z).
      fapply ax_sym. fapply add_rec_swap2. fapply ax_sym. fapply "Hz".
    Qed.
    Lemma PAle'_succ t x : Qeq ⊢ (x ⧀=' num t) → (x ⧀=' σ (num t)).
    Proof.
      fstart. fintros "[z Hz]". fexists (σ z).
      frewrite (ax_add_rec x z). fapply ax_succ_congr. ctx.
    Qed.

    Lemma add_zero_num t :
      Qeq ⊢ num t ⊕ zero == num t.
    Proof.
      induction t.
      - cbn. frewrite (ax_add_zero zero). fapply ax_refl.
      - cbn. frewrite (ax_add_rec zero (num t)).
        fapply ax_succ_congr. apply IHt.
    Qed.
    Lemma PAle_num_eq t x :
      Qeq ⊢ x == num t → x ⧀= num t.
    Proof.
      fstart. fintros "H". fexists zero.
      frewrite "H". fapply ax_sym. fapply add_zero_num.
    Qed.
    Lemma PAle'_num_eq t x :
      Qeq ⊢ x == num t → x ⧀=' num t.
    Proof.
      fstart. fintros "H". fexists zero.
      frewrite (ax_add_zero x). fapply ax_sym. fapply "H".
    Qed.

    Fixpoint fin_disj n φ := match n with
                             | 0 => φ[(num 0) ..]
                             | S n => (fin_disj n φ) ∨ φ[(num (S n)) ..]
                             end.
    Fixpoint fin_conj n φ := match n with
                             | 0 => φ[(num 0) ..]
                             | S n => (fin_conj n φ) ∧ φ[(num (S n)) ..]
                             end.

    Lemma le_fin_disj t x :
      Qeq ⊢ x ⧀= num t ↔ fin_disj t (x`[↑] == $0).
    Proof.
      induction t; cbn; rewrite subst_term_shift; fstart; fsplit.
      - fapply PAle_zero_eq.
      - fintros "H". unfold PAle.
        frewrite "H". fexists zero.
        frewrite (ax_add_zero zero). fapply ax_refl.
      - fintros "H". fassert (x == σ num t ∨ (¬ x == σ num t)) as "H1".
        { pose proof (Q_eqdec (S t) x). cbn in H. fapply H. }
        fdestruct "H1" as "[H1|H1]".
        + fright. ctx.
        + fleft. fapply IHt.
          fapply PAle_sigma_neq; ctx.
      - fintros "H". fdestruct "H" as "[H|H]".
        + fapply PAle_succ. fapply IHt. fapply "H".
        + pose proof (PAle_num_eq (S t) x). cbn in H.
          fapply H. fapply "H".
    Qed.
    Lemma le_swap_fin_disj t x :
      Qeq ⊢ x ⧀=' num t ↔ fin_disj t (x`[↑] == $0).
    Proof.
      induction t; cbn; rewrite subst_term_shift; fstart; fsplit.
      - fapply PAle'_zero_eq.
      - unfold PAle'.  fintros "H". frewrite "H".
        fexists zero. frewrite (ax_add_zero zero). fapply ax_refl.
      - fintros "H". fassert (x == σ num t ∨ (¬ x == σ num t)) as "H1".
        { pose proof (Q_eqdec (S t) x). cbn in H. fapply H. }
        fdestruct "H1" as "[H1|H1]".
        + fright. ctx.
        + fleft. fapply IHt.
          fapply PAle'_sigma_neq; ctx.
      - fintros "H". fdestruct "H" as "[H|H]".
        + fapply PAle'_succ. fapply IHt. fapply "H".
        + pose proof (PAle'_num_eq (S t) x). cbn in H.
          fapply H. fapply "H".
    Qed.

    Lemma Q_leibniz_t a x y : Qeq ⊢ x == y → a`[x..] == a`[y..].
    Proof.
      induction a.
      - destruct x0; cbn.
        + fintros. ctx.
        + fintros. fapply ax_refl.
      - destruct F.
        + cbn in v. rewrite (vec_0_nil v).
          fintros. fapply ax_refl.
        + cbn in v.
          destruct (vec_1_inv v) as [z ->]. cbn.
          fintros. fapply (ax_succ_congr z`[y..] z`[x..]).
          frevert 0. fapply IH. apply Vector.In_cons_hd.
        + destruct (vec_2_inv v) as (a & b & ->).
          cbn. fintros. fapply ax_add_congr.
          all: frevert 0; fapply IH.
          * apply Vector.In_cons_hd.
          * apply Vector.In_cons_tl, Vector.In_cons_hd.
        + destruct (vec_2_inv v) as (a & b & ->).
          cbn. fintros. fapply ax_mult_congr.
          all: frevert 0; fapply IH.
          * apply Vector.In_cons_hd.
          * apply Vector.In_cons_tl, Vector.In_cons_hd.
    Qed.

    Lemma Q_leibniz φ x y :
      Qeq ⊢ x == y → φ[x..] → φ[y..].
    Proof.
      enough (Qeq ⊢ x == y → φ[x..] ↔ φ[y..]).
      { fintros. fapply H; ctx. }
      induction φ using form_ind_subst.
      - cbn. fintros. fsplit; fintros; ctx.
      - destruct P0. cbn in t.
        destruct (vec_2_inv t) as (a & b & ->).
        cbn. fstart. fintros.
        fassert (a`[x..] == a`[y..]).
        { pose proof (Q_leibniz_t a x y).
          fapply H. fapply "H". }
        fassert (b`[x..] == b`[y..]).
        { pose proof (Q_leibniz_t b x y).
          fapply H. fapply "H". }
        frewrite "H0". frewrite "H1".
        fsplit; fintros; ctx.
      - fstart; fintros.
        fassert (φ1[x..] ↔ φ1[y..]) by (fapply IHφ1; fapply "H").
        fassert (φ2[x..] ↔ φ2[y..]) by (fapply IHφ2; fapply "H").
        destruct b0; fsplit; cbn.
        + fintros "[H2 H3]". fsplit.
          * fapply "H0". ctx.
          * fapply "H1". ctx.
        + fintros "[H2 H3]". fsplit.
          * fapply "H0". ctx.
          * fapply "H1". ctx.
        + fintros "[H2|H3]".
          * fleft. fapply "H0". ctx.
          * fright. fapply "H1". ctx.
        + fintros "[H2|H3]".
          * fleft. fapply "H0". ctx.
          * fright. fapply "H1". ctx.
        + fintros "H2" "H3".
          fapply "H1". fapply "H2". fapply "H0". ctx.
        + fintros "H2" "H3".
          fapply "H1". fapply "H2". fapply "H0". ctx.
      - fstart. fintros. fsplit; destruct q; cbn; fintros.
        + specialize (H (x0`[↑]..)).
          asimpl in H. asimpl. fapply H.
          * ctx.
          * fspecialize ("H0" x0). asimpl. ctx.
        + fdestruct "H0". fexists x0.
          specialize (H (x0`[↑]..)).
          asimpl in H. asimpl. fapply H; ctx.
        + specialize (H (x0`[↑]..)).
          asimpl in H. asimpl. fapply H.
          * ctx.
          * fspecialize ("H0" x0). asimpl. ctx.
        + fdestruct "H0". fexists x0.
          specialize (H (x0`[↑]..)).
          asimpl in H. asimpl. fapply H; ctx.
    Qed.

    (* Could probably be generalised to arbitrary finite disjunctions *)
    Lemma forall_fin_disj_conj φ t :
      Qeq ⊢ (∀ (fin_disj t ($1 == $0)) → φ) ↔ fin_conj t φ.
    Proof.
      induction t as [|t IH]; cbn; fstart; fsplit.
      - fintros "H". fapply "H". fapply ax_refl.
      - fintros "H" x "H1".
        feapply Q_leibniz.
        + feapply ax_sym. fapply "H1".
        + ctx.
      - fintros "H". fsplit.
        + fapply IH. fintros x "H1". fapply "H". fleft. fapply "H1".
        + fapply "H". fright. rewrite num_subst. fapply ax_refl.
      - fintros "[H1 H2]" x "[H3|H3]".
        + fdestruct IH as "[H4 H5]".
          fapply "H5"; ctx.
        + rewrite num_subst. feapply Q_leibniz.
          * feapply ax_sym. fapply "H3".
          * fapply "H2".
    Qed.

    Lemma exists_fin_disj φ t :
      Qeq ⊢ (∃ (fin_disj t ($1 == $0)) ∧ φ) ↔ fin_disj t φ.
    Proof.
      induction t as [|t IH]; cbn; fstart; fsplit.
      - fintros "[x [H1 H2]]". feapply Q_leibniz.
        + fapply "H1".
        + ctx.
      - fintros "H". fexists zero. fsplit.
        + fapply ax_refl.
        + ctx.
      - fintros "[x [[H1|H1] H2]]".
        + fleft. fapply IH. fexists x. fsplit.
          * fapply "H1".
          * fapply "H2".
        + fright. rewrite num_subst. feapply Q_leibniz.
          * fapply "H1".
          * ctx.
      - fintros "[H1|H1]".
        + fapply IH in "H1". fdestruct "H1" as "[x [H1 H2]]".
          fexists x. fsplit.
          * fleft. ctx.
          * ctx.
        + fexists (σ num t). fsplit.
          * fright. rewrite num_subst. fapply ax_refl.
          * ctx.
    Qed.

    Lemma forall_bound_iff φ ψ χ:
      Qeq ⊢ φ ↔ ψ -> Qeq ⊢ (∀ φ → χ) ↔ (∀ ψ → χ).
    Proof.
      intros H. fstart. fsplit.
      - fintros "H1" x "H2". fapply "H1".
        apply (subst_Weak x..) in H. change (List.map _ _) with Qeq in H.
        cbn in H. fapply H. fapply "H2".
      - fintros "H1" x "H2". fapply "H1".
        apply (subst_Weak x..) in H. change (List.map _ _) with Qeq in H.
        cbn in H. fapply H. fapply "H2".
    Qed.

  End lemmas.

  Lemma Qdec_fin_conj φ t :
    Qdec φ -> Qdec (fin_conj t φ).
  Proof.
    intros Hφ. induction t; cbn.
    - apply Qdec_subst, Hφ.
    - apply Qdec_and.
      + assumption.
      + apply Qdec_subst, Hφ.
  Qed.

  Lemma Qdec_fin_disj φ t :
    Qdec φ -> Qdec (fin_disj t φ).
  Proof.
    intros Hφ. induction t; cbn.
    - apply Qdec_subst, Hφ.
    - apply Qdec_or.
      + assumption.
      + apply Qdec_subst, Hφ.
  Qed.
  Lemma fin_disj_subst n φ ρ :
    (fin_disj n φ)[ρ] = fin_disj n φ[up ρ].
  Proof.
    induction n; cbn.
    - now asimpl.
    - cbn. f_equal; first assumption.
      asimpl. now rewrite num_subst.
  Qed.

  Theorem Qdec_bounded_forall t φ :
    Qdec φ -> Qdec (∀ $0 ⧀= t`[↑] → φ).
  Proof.
    intros H pei ρ Hρ.
    destruct (@closed_term_is_num _ t`[ρ]) as [x Hx].
    { apply subst_t_closed, Hρ. }
    enough (Qeq ⊢ (∀ (fin_disj x ($1 == $0))  → φ)[ρ] \/ Qeq ⊢ ¬ (∀ (fin_disj x ($1 == $0)) → φ)[ρ]) as H'.
    { cbn. asimpl. rewrite <-!subst_term_comp.
      cbn in H'. rewrite fin_disj_subst in H'.
      cbn in H'. unfold "↑" in H'.
      destruct H' as [H1|H1].
      - left. fstart. fintros. fapply H1.
        rewrite fin_disj_subst. cbn.
        fapply le_fin_disj.
        fdestruct "H" as "[z H]". fexists z.
        fassert (t`[ρ] == num x); first fapply Hx.
        frewrite <-"H0". asimpl. fapply "H".
      - right.  fstart. fintros. fapply H1. fstop.
        fintros. fstart.
        fapply "H".
        rewrite fin_disj_subst. cbn.
        fassert (x0 ⧀= num x).
        { fapply le_fin_disj. fapply "H0". }
        fdestruct "H1" as "[z Hz]".
        fexists z.
        fassert (t`[ρ] == num x); first fapply Hx.
        asimpl. frewrite "H1". fapply "Hz". }
    eapply Qdec_iff.
    - apply frewrite_equiv_switch. apply forall_fin_disj_conj.
    - apply Qdec_fin_conj, H.
    - apply Hρ.
  Qed.
  Theorem Qdec_bounded_exists t φ :
    Qdec φ -> Qdec (∃ ($0 ⧀= t`[↑]) ∧ φ).
  Proof.
    intros H pei ρ Hρ.
    destruct (@closed_term_is_num _ t`[ρ]) as [x Hx].
    { apply subst_t_closed, Hρ. }
    enough (Qeq ⊢ (∃ (fin_disj x ($1 == $0)) ∧ φ)[ρ] \/ Qeq ⊢ ¬ (∃ (fin_disj x ($1 == $0)) ∧ φ)[ρ]) as H'.
    { cbn.
      cbn in H'. rewrite fin_disj_subst in H'.
      cbn in H'. unfold "↑" in H'.
      destruct H' as [H1|H1].
      - left. fstart.
        fassert (∃ fin_disj x ($1 == $0) ∧ φ[up ρ]).
        { fapply H1. }
        fdestruct "H" as "[z [H1 H2]]".
        rewrite fin_disj_subst. cbn.
        fexists z. fsplit; last ctx.
        fassert (z ⧀= num x).
        { fapply le_fin_disj. fapply "H1". }
        unfold PAle. fdestruct "H". fexists x0.
        asimpl. frewrite Hx. fapply "H".
      - right.  fstart. fintros. fapply H1.
        fdestruct "H" as "[z [H1 H2]]". fexists z.
        fsplit; last ctx.
        rewrite fin_disj_subst. cbn. fapply le_fin_disj.
        cbn. fdestruct "H1" as "[z' Hz']". fexists z'.
        fassert (t`[ρ] == num x) by fapply Hx.
        asimpl. frewrite <-"H". fapply "Hz'". }
    eapply Qdec_iff.
    - apply frewrite_equiv_switch. apply exists_fin_disj.
    - apply Qdec_fin_disj, H.
    - apply Hρ.
  Qed.

  Theorem Qdec_bounded_exists_comm t φ :
    Qdec φ -> Qdec (∃ ($0 ⧀=' t`[↑]) ∧ φ).
  Proof.
    intros H pei ρ Hρ.
    destruct (@closed_term_is_num _ t`[ρ]) as [x Hx].
    { apply subst_t_closed, Hρ. }
    enough (Qeq ⊢ (∃ (fin_disj x ($1 == $0)) ∧ φ)[ρ] \/ Qeq ⊢ ¬ (∃ (fin_disj x ($1 == $0)) ∧ φ)[ρ]) as H'.
    { cbn.
      cbn in H'. rewrite fin_disj_subst in H'.
      cbn in H'. unfold "↑" in H'.
      destruct H' as [H1|H1].
      - left. fstart.
        fassert (∃ fin_disj x ($1 == $0) ∧ φ[up ρ]) by apply H1.
        fdestruct "H" as "[z [H1 H2]]".
        rewrite fin_disj_subst. cbn.
        fexists z. fsplit; last ctx.
        fassert (z ⧀=' num x).
        { fapply le_swap_fin_disj. fapply "H1". }
        unfold PAle'. fdestruct "H". fexists x0.
        asimpl. frewrite Hx. fapply "H".
      - right.  fstart. fintros. fapply H1.
        fdestruct "H" as "[z [H1 H2]]". fexists z.
        fsplit; last ctx.
        rewrite fin_disj_subst. cbn. fapply le_swap_fin_disj.
        cbn. fdestruct "H1". fexists x0.
        fassert (t`[ρ] == num x) by fapply Hx.
        asimpl. frewrite <-"H0". fapply "H". }
    eapply Qdec_iff.
    - apply frewrite_equiv_switch. apply exists_fin_disj.
    - apply Qdec_fin_disj, H.
    - apply Hρ.
  Qed.
End Qdec.

author: uds-psl

repo: coq-synthetic-incompleteness


text:
Require Import Refinement.Prog.

Extraction Language Haskell.

Extract Constant opT "a" => "()".
Extract Constant world => "()".

Extract Inductive prog => "TheProg"
                           ["prim_error" "return" "(>>=)"]
                           "(\fprim fret fbind -> error 'pattern match on prog')".

author: mit-pdos

repo: deepspec-pocs

save_path: github-repos/coq/mit-pdos-deepspec-pocs