text:
Require Import Logic.GeneralLogic.Base.
Require Import Logic.MinimumLogic.Syntax.
Require Import Logic.MinimumLogic.ProofTheory.Minimum.
Require Import Logic.MinimumLogic.ProofTheory.RewriteClass.
Require Import Logic.MinimumLogic.Syntax.
Require Import Logic.MinimumLogic.ProofTheory.Minimum.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.ProofTheory.Intuitionistic.
Require Import Logic.PropositionalLogic.ProofTheory.DeMorgan.
Require Import Logic.PropositionalLogic.ProofTheory.GodelDummett.
Require Import Logic.PropositionalLogic.ProofTheory.Classical.
Require Import Logic.SeparationLogic.Syntax.
Require Import Logic.SeparationLogic.ProofTheory.SeparationLogic.
Require Import Logic.SeparationLogic.ProofTheory.TheoryOfSeparationAxioms.
Require Import Logic.SeparationLogic.DeepEmbedded.Parameter.
Require Logic.SeparationLogic.DeepEmbedded.SeparationLanguage.
Require Logic.SeparationLogic.DeepEmbedded.SeparationEmpLanguage.

Local Open Scope logic_base.
Local Open Scope syntax.
Import PropositionalLanguageNotation.
Import SeparationLogicNotation.

Module ReynoldsLogic.
Section ReynoldsLogic.

Context {Sigma: SeparationLanguage.PropositionalVariables}.

Existing Instances SeparationLanguage.L SeparationLanguage.minL SeparationLanguage.pL SeparationLanguage.sepconL  SeparationLanguage.wandL.

Inductive provable: SeparationLanguage.expr Sigma -> Prop :=
| modus_ponens: forall x y, provable (x --> y) -> provable x -> provable y
| axiom1: forall x y, provable (x --> (y --> x))
| axiom2: forall x y z, provable ((x --> y --> z) --> (x --> y) --> (x --> z))
| andp_intros: forall x y, provable (x --> y --> x && y)
| andp_elim1: forall x y, provable (x && y --> x)
| andp_elim2: forall x y, provable (x && y --> y)
| orp_intros1: forall x y, provable (x --> x || y)
| orp_intros2: forall x y, provable (y --> x || y)
| orp_elim: forall x y z, provable ((x --> z) --> (y --> z) --> (x || y --> z))
| falsep_elim: forall x, provable (FF --> x)
| sepcon_comm: forall x y, provable (x * y <--> y * x)
| sepcon_assoc: forall x y z, provable (x * (y * z) <--> (x * y) * z)
| wand_sepcon_adjoint1: forall x y z, provable (x * y --> z) -> provable (x --> (y -* z))
| wand_sepcon_adjoint2: forall x y z, provable (x --> (y -* z)) -> provable (x * y --> z)
| sepcon_elim1: forall x y, provable (x * y --> x).

Instance GP: Provable SeparationLanguage.L := Build_Provable _ provable.

Instance GD: Derivable SeparationLanguage.L := Provable2Derivable.

Instance AX: NormalAxiomatization SeparationLanguage.L GP GD :=
  Provable2Derivable_Normal.

Instance minAX: MinimumAxiomatization SeparationLanguage.L GP.
Proof.
  constructor.
  + apply modus_ponens.
  + apply axiom1.
  + apply axiom2.
Qed.

Instance ipAX: IntuitionisticPropositionalLogic SeparationLanguage.L GP.
Proof.
  constructor.
  + apply andp_intros.
  + apply andp_elim1.
  + apply andp_elim2.
  + apply orp_intros1.
  + apply orp_intros2.
  + apply orp_elim.
  + apply falsep_elim.
Qed.

Instance wandAX: WandAxiomatization SeparationLanguage.L GP.
Proof.
  constructor.
  intros; split.
  + apply wand_sepcon_adjoint1.
  + apply wand_sepcon_adjoint2.
Qed.

Instance sepconAX: SepconAxiomatization SeparationLanguage.L GP.
Proof.
  assert (SepconAxiomatization_weak_iffp SeparationLanguage.L GP).
  {
    constructor.
    + apply sepcon_comm.
    + apply sepcon_assoc.
  }
  eapply @SepconAxiomatizationWeakIff2SepconAxiomatizationWeak in H;
  try typeclasses eauto.
  eapply @SepconAxiomatizationWeak2SepconAxiomatization;
  try typeclasses eauto.
  eapply @Adj2SepconMono;
  try typeclasses eauto.
Qed.

Instance gcsAX: GarbageCollectSeparationLogic SeparationLanguage.L GP.
Proof.
  constructor.
  apply sepcon_elim1.
Qed.

End ReynoldsLogic.
End ReynoldsLogic.

Module OHearnLogic.
Section OHearnLogic.

Context {Sigma: SeparationEmpLanguage.PropositionalVariables}.

Existing Instances SeparationEmpLanguage.L SeparationEmpLanguage.minL SeparationEmpLanguage.pL SeparationEmpLanguage.sepconL SeparationEmpLanguage.wandL SeparationEmpLanguage.empL.

Inductive provable: SeparationEmpLanguage.expr Sigma -> Prop :=
| modus_ponens: forall x y, provable (x --> y) -> provable x -> provable y
| axiom1: forall x y, provable (x --> (y --> x))
| axiom2: forall x y z, provable ((x --> y --> z) --> (x --> y) --> (x --> z))
| andp_intros: forall x y, provable (x --> y --> x && y)
| andp_elim1: forall x y, provable (x && y --> x)
| andp_elim2: forall x y, provable (x && y --> y)
| orp_intros1: forall x y, provable (x --> x || y)
| orp_intros2: forall x y, provable (y --> x || y)
| orp_elim: forall x y z, provable ((x --> z) --> (y --> z) --> (x || y --> z))
| falsep_elim: forall x, provable (FF --> x)
| excluded_middle: forall x, provable (x || ~~ x)
| sepcon_comm: forall x y, provable (x * y <--> y * x)
| sepcon_assoc: forall x y z, provable (x * (y * z) <--> (x * y) * z)
| wand_sepcon_adjoint1: forall x y z, provable (x * y --> z) -> provable (x --> (y -* z))
| wand_sepcon_adjoint2: forall x y z, provable (x --> (y -* z)) -> provable (x * y --> z)
| sepcon_emp: forall x, provable (x * emp <--> x).

Instance GP: Provable SeparationEmpLanguage.L := Build_Provable _ provable.

Instance GD: Derivable SeparationEmpLanguage.L := Provable2Derivable.

Instance AX: NormalAxiomatization SeparationEmpLanguage.L GP GD :=
  Provable2Derivable_Normal.

Instance minAX: MinimumAxiomatization SeparationEmpLanguage.L GP.
Proof.
  constructor.
  + apply modus_ponens.
  + apply axiom1.
  + apply axiom2.
Qed.

Instance ipAX: IntuitionisticPropositionalLogic SeparationEmpLanguage.L GP.
Proof.
  constructor.
  + apply andp_intros.
  + apply andp_elim1.
  + apply andp_elim2.
  + apply orp_intros1.
  + apply orp_intros2.
  + apply orp_elim.
  + apply falsep_elim.
Qed.

Instance cpAX: ClassicalPropositionalLogic SeparationEmpLanguage.L GP.
Proof.
  constructor.
  apply excluded_middle.
Qed.

Instance wandAX: WandAxiomatization SeparationEmpLanguage.L GP.
Proof.
  constructor.
  intros; split.
  + apply wand_sepcon_adjoint1.
  + apply wand_sepcon_adjoint2.
Qed.

Instance sepconAX: SepconAxiomatization SeparationEmpLanguage.L GP.
Proof.
  assert (SepconAxiomatization_weak_iffp SeparationEmpLanguage.L GP).
  {
    constructor.
    + apply sepcon_comm.
    + apply sepcon_assoc.
  }
  eapply @SepconAxiomatizationWeakIff2SepconAxiomatizationWeak in H;
  try typeclasses eauto.
  eapply @SepconAxiomatizationWeak2SepconAxiomatization;
  try typeclasses eauto.
  eapply @Adj2SepconMono;
  try typeclasses eauto.
Qed.

Instance empAX: EmpAxiomatization SeparationEmpLanguage.L GP.
Proof.
  eapply @EmpAxiomatizationIff2EmpAxiomatization;
  try typeclasses eauto.
  constructor.
  apply sepcon_emp.
Qed.

End OHearnLogic.
End OHearnLogic.

Module LogicOnModuResModel.
Section LogicOnModuResModel.

Context {Sigma: SeparationEmpLanguage.PropositionalVariables}.

Existing Instances SeparationEmpLanguage.L SeparationEmpLanguage.minL SeparationEmpLanguage.pL SeparationEmpLanguage.sepconL SeparationEmpLanguage.wandL SeparationEmpLanguage.empL.

Inductive provable: SeparationEmpLanguage.expr Sigma -> Prop :=
| modus_ponens: forall x y, provable (x --> y) -> provable x -> provable y
| axiom1: forall x y, provable (x --> (y --> x))
| axiom2: forall x y z, provable ((x --> y --> z) --> (x --> y) --> (x --> z))
| andp_intros: forall x y, provable (x --> y --> x && y)
| andp_elim1: forall x y, provable (x && y --> x)
| andp_elim2: forall x y, provable (x && y --> y)
| orp_intros1: forall x y, provable (x --> x || y)
| orp_intros2: forall x y, provable (y --> x || y)
| orp_elim: forall x y z, provable ((x --> z) --> (y --> z) --> (x || y --> z))
| falsep_elim: forall x, provable (FF --> x)
| sepcon_comm: forall x y, provable (x * y <--> y * x)
| sepcon_assoc: forall x y z, provable (x * (y * z) <--> (x * y) * z)
| wand_sepcon_adjoint1: forall x y z, provable (x * y --> z) -> provable (x --> (y -* z))
| wand_sepcon_adjoint2: forall x y z, provable (x --> (y -* z)) -> provable (x * y --> z)
| sepcon_emp: forall x, provable (x * emp <--> x)
| sepcon_elim1: forall x y, provable (x * y --> x).

Instance GP: Provable SeparationEmpLanguage.L := Build_Provable _ provable.

Instance GD: Derivable SeparationEmpLanguage.L := Provable2Derivable.

Instance AX: NormalAxiomatization SeparationEmpLanguage.L GP GD :=
  Provable2Derivable_Normal.

Instance minAX: MinimumAxiomatization SeparationEmpLanguage.L GP.
Proof.
  constructor.
  + apply modus_ponens.
  + apply axiom1.
  + apply axiom2.
Qed.

Instance ipAX: IntuitionisticPropositionalLogic SeparationEmpLanguage.L GP.
Proof.
  constructor.
  + apply andp_intros.
  + apply andp_elim1.
  + apply andp_elim2.
  + apply orp_intros1.
  + apply orp_intros2.
  + apply orp_elim.
  + apply falsep_elim.
Qed.

Instance wandAX: WandAxiomatization SeparationEmpLanguage.L GP.
Proof.
  constructor.
  intros; split.
  + apply wand_sepcon_adjoint1.
  + apply wand_sepcon_adjoint2.
Qed.

Instance sepconAX: SepconAxiomatization SeparationEmpLanguage.L GP.
Proof.
  assert (SepconAxiomatization_weak_iffp SeparationEmpLanguage.L GP).
  {
    constructor.
    + apply sepcon_comm.
    + apply sepcon_assoc.
  }
  eapply @SepconAxiomatizationWeakIff2SepconAxiomatizationWeak in H;
  try typeclasses eauto.
  eapply @SepconAxiomatizationWeak2SepconAxiomatization;
  try typeclasses eauto.
  eapply @Adj2SepconMono;
  try typeclasses eauto.
Qed.

Instance empAX: EmpAxiomatization SeparationEmpLanguage.L GP.
Proof.
  eapply @EmpAxiomatizationIff2EmpAxiomatization;
  try typeclasses eauto.
  constructor.
  apply sepcon_emp.
Qed.

Instance gcsAX: GarbageCollectSeparationLogic SeparationEmpLanguage.L GP.
Proof.
  constructor.
  apply sepcon_elim1.
Qed.

End LogicOnModuResModel.
End LogicOnModuResModel.

Module LogicOnMSL.
Section LogicOnMSL.

Context {Sigma: SeparationEmpLanguage.PropositionalVariables}.

Existing Instances SeparationEmpLanguage.L SeparationEmpLanguage.minL SeparationEmpLanguage.pL SeparationEmpLanguage.sepconL SeparationEmpLanguage.wandL SeparationEmpLanguage.empL.

Inductive provable: SeparationEmpLanguage.expr Sigma -> Prop :=
| modus_ponens: forall x y, provable (x --> y) -> provable x -> provable y
| axiom1: forall x y, provable (x --> (y --> x))
| axiom2: forall x y z, provable ((x --> y --> z) --> (x --> y) --> (x --> z))
| andp_intros: forall x y, provable (x --> y --> x && y)
| andp_elim1: forall x y, provable (x && y --> x)
| andp_elim2: forall x y, provable (x && y --> y)
| orp_intros1: forall x y, provable (x --> x || y)
| orp_intros2: forall x y, provable (y --> x || y)
| orp_elim: forall x y z, provable ((x --> z) --> (y --> z) --> (x || y --> z))
| falsep_elim: forall x, provable (FF --> x)
| impp_choice: forall x y, provable ((x --> y) || (y --> x))
| sepcon_comm: forall x y, provable (x * y <--> y * x)
| sepcon_assoc: forall x y z, provable (x * (y * z) <--> (x * y) * z)
| wand_sepcon_adjoint1: forall x y z, provable (x * y --> z) -> provable (x --> (y -* z))
| wand_sepcon_adjoint2: forall x y z, provable (x --> (y -* z)) -> provable (x * y --> z)
| sepcon_emp: forall x, provable (x * emp <--> x).

Instance GP: Provable SeparationEmpLanguage.L := Build_Provable _ provable.

Instance GD: Derivable SeparationEmpLanguage.L := Provable2Derivable.

Instance AX: NormalAxiomatization SeparationEmpLanguage.L GP GD :=
  Provable2Derivable_Normal.

Instance minAX: MinimumAxiomatization SeparationEmpLanguage.L GP.
Proof.
  constructor.
  + apply modus_ponens.
  + apply axiom1.
  + apply axiom2.
Qed.

Instance ipAX: IntuitionisticPropositionalLogic SeparationEmpLanguage.L GP.
Proof.
  constructor.
  + apply andp_intros.
  + apply andp_elim1.
  + apply andp_elim2.
  + apply orp_intros1.
  + apply orp_intros2.
  + apply orp_elim.
  + apply falsep_elim.
Qed.

Instance wandAX: WandAxiomatization SeparationEmpLanguage.L GP.
Proof.
  constructor.
  intros; split.
  + apply wand_sepcon_adjoint1.
  + apply wand_sepcon_adjoint2.
Qed.

Instance sepconAX: SepconAxiomatization SeparationEmpLanguage.L GP.
Proof.
  assert (SepconAxiomatization_weak_iffp SeparationEmpLanguage.L GP).
  {
    constructor.
    + apply sepcon_comm.
    + apply sepcon_assoc.
  }
  eapply @SepconAxiomatizationWeakIff2SepconAxiomatizationWeak in H;
  try typeclasses eauto.
  eapply @SepconAxiomatizationWeak2SepconAxiomatization;
  try typeclasses eauto.
  eapply @Adj2SepconMono;
  try typeclasses eauto.
Qed.

Instance empAX: EmpAxiomatization SeparationEmpLanguage.L GP.
Proof.
  eapply @EmpAxiomatizationIff2EmpAxiomatization;
  try typeclasses eauto.
  constructor.
  apply sepcon_emp.
Qed.

End LogicOnMSL.
End LogicOnMSL.

author: QinxiangCao

repo: UnifySL

save_path: github-repos/coq/QinxiangCao-UnifySL


text:
Require Export Coq.Lists.List. Export ListNotations.
Require Export Coq.ZArith.ZArith. Open Scope Z_scope.
Require Export coqutil.Word.Interface coqutil.Word.Properties.
Require Export coqutil.Map.Interface coqutil.Map.Properties.
Require Import coqutil.Tactics.rdelta coqutil.Tactics.destr coqutil.Decidable.
Require Import coqutil.Tactics.rewr coqutil.Tactics.Tactics.
Require Import coqutil.Tactics.ltac_list_ops.
Require Export coqutil.Z.Lia.
Require Export coqutil.Datatypes.PropSet.
Require Export bedrock2.Lift1Prop.
Require Export bedrock2.Map.Separation.
Require Export bedrock2.Map.SeparationLogic.
Require Export bedrock2.Array.
Require Export bedrock2.Scalars.
Require Export bedrock2.ptsto_bytes.
Require Export coqutil.Word.SimplWordExpr.
Require Import coqutil.Tactics.Simp.

Lemma f_equal2: forall {A B: Type} {f1 f2: A -> B} {a1 a2: A},
    f1 = f2 -> a1 = a2 -> f1 a1 = f2 a2.
Proof. intros. congruence. Qed.

(* unifies two separation logic clauses syntactically, instantiating as many evars
   as it wants, but for subterms of type word, applies word solver instead of syntatic unify,
   and for subterms of type Z, applies lia instead of syntactic unify *)
Ltac wclause_unify OK :=
  lazymatch type of OK with
  | word.ok ?WORD =>
    lazymatch goal with
    | |- @eq ?T ?x ?y =>
      tryif first [is_evar x | is_evar y | constr_eq x y] then (
        reflexivity
      ) else (
        tryif (unify T (@word.rep _ WORD)) then (
          solve [solve_word_eq OK]
        ) else (
          tryif (unify T Z) then (
            solve [blia]
          ) else (
            lazymatch x with
            | ?x1 ?x2 => lazymatch y with
                         | ?y1 ?y2 => refine (f_equal2 _ _); wclause_unify OK
                         | _ => fail "" x "is an application while" y "is not"
                         end
            | _ => lazymatch y with
                   | ?y1 ?y2 => fail "" x "is not an application while" y "is"
                   | _ => tryif constr_eq x y then reflexivity else fail "" x "does not match" y
                   end
            end
          )
        )
      )
    end
  | _ => fail 1000 "OK does not have the right type"
  end.

(* This can be overridden by the user.
   The idea of a "tag" is that it's a subterm of a sepclause which is so unique that if
   the same tag appears both on the left and on the right of an iff1, we're sure that
   these two clauses should be matched & canceled with each other.
   "tag" should return any Gallina term. *)
Ltac tag P :=
  let __ := lazymatch type of P with
            | @map.rep _ _ _ -> Prop => idtac
            | _ => fail 10000 P "is not a sep clause"
            end in
  lazymatch P with
  | _ => fail "no recognizable tag"
  end.

(* This can be overridden by the user.
   The idea of "addr" is that if the addresses of two sepclauses are the same,
   we're sure that these two clauses should be matched & canceled with each other,
   even if they still contain many evars outside of their address.
   "addr" should return a Gallina term of type "word" *)
Ltac addr P :=
  let __ := lazymatch type of P with
            | @map.rep _ _ _ -> Prop => idtac
            | _ => fail 10000 P "is not a sep clause"
            end in
  lazymatch P with
  | ptsto ?A _ => A
  | ptsto_bytes _ ?A _ => A
  | ptsto_word ?A _ => A
  | array _ _ ?A _ => A
  | _ => fail "no recognizable address"
  end.

(* completely solves a sepclause equality or fails *)
Ltac sepclause_eq OK :=
  match goal with
  | |- ?G => assert_fails (has_evar G);
             wclause_unify OK
  | |- ?lhs = ?rhs => let tagL := tag lhs in
                      let tagR := tag rhs in
                      constr_eq tagL tagR;
                      wclause_unify OK
  | |- ?lhs = ?rhs => let addrL := addr lhs in
                      let addrR := addr rhs in
                      assert_fails (has_evar addrL);
                      assert_fails (has_evar addrR);
                      replace addrL with addrR by solve_word_eq OK;
                      (reflexivity || fail 10000 lhs "and" rhs "have the same address"
                      "according to addr, but can't be matched")
  end.

Ltac pick_nat n :=
  multimatch n with
  | S ?m => constr:(m)
  | S ?m => pick_nat m
  end.

Ltac wcancel_step OK := once (
  let RHS := lazymatch goal with |- Lift1Prop.iff1 _ (seps ?RHS) => RHS end in
  let jy := index_and_element_of RHS in (* <-- multi-success! *)
  let j := lazymatch jy with (?i, _) => i end in
  let y := lazymatch jy with (_, ?y) => y end in
  assert_fails (idtac; let y := rdelta_var y in is_evar y);
  let LHS := lazymatch goal with |- Lift1Prop.iff1 (seps ?LHS) _ => LHS end in
  let l := eval cbv [List.length] in (List.length LHS) in
  let i := pick_nat l in (* <-- multi-success! *)
  cancel_seps_at_indices i j; [sepclause_eq OK|]).

Ltac word_rep_to_word_ok R :=
  lazymatch constr:(@eq R (word.of_Z 0)) with
  | @eq _ (@word.of_Z _ ?Inst _) => constr:(_: word.ok Inst)
  end.

Ltac wcancel :=
  cancel;
  let OK := lazymatch goal with
            | |- @iff1 (@map.rep (@word.rep ?W ?WordInst) ?V ?M) _ _ =>
              constr:(_: word.ok WordInst)
            end in
  repeat wcancel_step OK;
  try solve [ecancel_done'].

(* mostly useful for debugging, once everything works, wcancel should do all the work *)
Ltac cancel_by_tag :=
  let RHS := lazymatch goal with |- Lift1Prop.iff1 _ (seps ?RHS) => RHS end in
  let jy := index_and_element_of RHS in
  let j := lazymatch jy with (?i, _) => i end in
  let y := lazymatch jy with (_, ?y) => y end in
  let tagR := tag y in
  assert_fails (idtac; let y := rdelta_var y in is_evar y);
  let LHS := lazymatch goal with |- Lift1Prop.iff1 (seps ?LHS) _ => LHS end in
  let l := eval cbv [List.length] in (List.length LHS) in
  let i := pick_nat l in
  let x := eval cbv [List.nth] in (List.nth i LHS (emp True)) in
  let tagL := tag x in
  constr_eq tagL tagR;
  cancel_seps_at_indices i j.

Ltac simpl_addrs :=
  (* note: it's the user's responsability to ensure that left-to-right rewriting with all
   nat and Z equations terminates, otherwise we'll loop infinitely here *)
  repeat match goal with
         | E: @eq ?T ?LHS _ |- _ =>
           lazymatch T with
           | Z => idtac
           | nat => idtac
           end;
           progress prewrite LHS E
         (* inside the loop because the above rewriting can create new opportunities for simpl_Z_nat *)
         | |- _ => progress simpl_Z_nat
         end.

(* Note that "rewr" only works with equalities, not with iff1, so we use
   iff1ToEq to turn iff1 into eq (requires functional and propositionl extensionality).
   Alternatively, we could use standard rewrite (which might instantiate too many evars),
   or we could make a "seprewrite" which works on "seps [...] [...]" by replacing the
   i-th clause on any side with the rhs of the provided iff1, or we could make a
   seprewrite which first puts the clause to be replaced as the left-most, and then
   eapplies a "Proper_sep_iff1: Proper (iff1 ==> iff1 ==> iff1) sep", but that would
   change the order of the clauses. *)
Ltac get_array_rewr_eq t :=
  lazymatch t with
  | context [ array ?PT ?SZ ?start (?xs ++ ?ys) ] =>
    constr:(iff1ToEq (array_append' PT SZ xs ys start))
  | context [ array ?PT ?SZ ?start (?x :: ?xs) ] =>
    constr:(iff1ToEq (array_cons PT SZ x xs start))
  | context [ array ?PT ?SZ ?start nil ] =>
    constr:(iff1ToEq (array_nil PT SZ start))
  end.

Ltac array_app_cons_sep := rewr get_array_rewr_eq in *.

Ltac wseplog_pre :=
  repeat (autounfold with unf_to_array);
  repeat ( rewr get_array_rewr_eq in |-* ).

Ltac wwcancel :=
  wseplog_pre;
  simpl_addrs;
  wcancel.

Ltac wcancel_assumption := use_sep_assumption; wwcancel.

author: mit-plv


text:
(**
CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.

- Frederic Blanqui, 2005-02-17

general lemmas and tactics
*)

Set Implicit Arguments.

From Coq Require Import Structures.Equalities.
From Coq Require Export EqdepFacts Eqdep_dec.
From Coq Require Setoid.

From CoLoR Require Import LogicUtil RelUtil BoolUtil.

(***********************************************************************)
(** Functor providing properties the basic properties of Leibniz
equality on some type. *)

Module LeibnizFacts (Import T : Typ).

  Definition eq : relation t := @Logic.eq t.

  Instance eq_refl : Reflexive eq.

  Proof. fo. Qed.

  Instance eq_sym : Symmetric eq.

  Proof. fo. Qed.

  Instance eq_trans : Transitive eq.

  Proof. unfold eq; class. Qed.

End LeibnizFacts.

(***********************************************************************)
(** Type equipped with a boolean equility. *)

Record Bool_eq_type : Type := mkBool_eq_type {
  bet_type :> Type;
  bet_eq : bet_type -> bet_type -> bool;
  bet_ok : forall x y, bet_eq x y = true <-> x = y }.

(***********************************************************************)
(** Properties of Leibniz equality on decidable types. *)

Section eq_dep.

  Variables (A : Type) (eq_dec : forall x y : A, {x=y}+{~x=y}).

  Lemma eq_rect_eq : forall (p : A) Q x h, x = eq_rect p Q x p h.

  Proof. exact (eq_rect_eq_dec eq_dec). Qed.

  Lemma eq_dep_eq : forall P (p : A) x y, eq_dep A P p x p y -> x = y.

  Proof. exact (eq_rect_eq__eq_dep_eq A eq_rect_eq). Qed.

  Lemma UIP : forall (x y : A) (p1 p2 : x = y), p1 = p2.

  Proof. exact (eq_dep_eq__UIP A eq_dep_eq). Qed.

  Lemma UIP_refl : forall (x : A) (p : x = x), p = eq_refl x.

  Proof. exact (UIP__UIP_refl A UIP). Qed.

  Lemma Streicher_K :
    forall (x : A) (P : x = x -> Prop), P (eq_refl x) -> forall p, P p.

  Proof. exact (K_dec_type eq_dec). Qed.

  Lemma inj_existT :
    forall P (x : A) (p q : P x), existT p = existT q -> p = q.

  Proof. exact (eq_dep_eq__inj_pairT2 A eq_dep_eq). Qed.

  Lemma inj_ex_intro :
    forall P (x : A) p q, ex_intro P x p = ex_intro P x q -> p = q.

  Proof.
    intros. apply inj_right_pair with (A:=A).
    intros x0 y0; case (eq_dec x0 y0); [left|right]; hyp.
    hyp.
  Qed.

End eq_dep.

Arguments UIP_refl [A] _ [x] p.

(***********************************************************************)
(** Properties of a boolean function testing Leibniz equality. *)

Section beq.

  Variable A : Type.
  Variable beq : A -> A -> bool.
  Variable beq_ok : forall x y, beq x y = true <-> x = y.

  Lemma beq_refl : forall x, beq x x = true.

  Proof. intro. ded (beq_ok x x). rewrite H. refl. Qed.

  Lemma beq_ko : forall x y, beq x y = false <-> x <> y.

  Proof.
    intros. destruct (beq_ok x y). case_eq (beq x y); intuition.
    rewrite H1 in H4. discr.
  Defined.

  Lemma dec_beq : forall x y : A, {x=y}+{~x=y}.

  Proof.
    intros. set (b := beq x y). case_eq b; intros.
    left. exact (proj1 (beq_ok x y) H).
    right. intro. unfold b in H. subst. rewrite beq_refl in H. discr.
  Defined.

  Lemma beq_com : forall x y, beq x y = beq y x.

  Proof.
    intros. case_eq (beq x y); intros; sym.
    rewrite beq_ok. sym. rewrite <- beq_ok. hyp.
    rewrite beq_ko. cut (x<>y). auto. rewrite <- beq_ko. hyp.
  Qed.

  Lemma beq_sym : forall x y, beq x y = true -> beq y x = true.

  Proof. intros. rewrite beq_com. exact H. Qed.

  Lemma beq_trans : forall x y z,
    beq x y = true -> beq y z = true -> beq x z = true.

  Proof.
    intros. rewrite beq_ok in H. rewrite beq_ok in H0.
    assert (x = z). apply eq_trans with y; hyp.
    rewrite beq_ok. exact H1.
  Qed.

End beq.

Arguments beq_refl [A beq] _ x.
Arguments dec_beq [A beq] _ x y.
Arguments beq_com [A beq] _ x y.
Arguments beq_ko [A beq] _ x y.

Ltac case_beq beq beq_ok x y := case_eq (beq x y);
  [let h := fresh in intro h; rewrite beq_ok in h;
    match type of h with ?x = ?y => subst y end
    | intro].

(***********************************************************************)
(** Boolean function testing Leibniz equality when it is decidable. *)

Section eq_dec.

  Variable A : Type.
  Variable eq_dec : forall x y : A, {x=y}+{~x=y}.

  Definition beq_dec x y :=
    match eq_dec x y with
      | left _ => true
      | right _ => false
    end.

  Lemma beq_dec_ok : forall x y, beq_dec x y = true <-> x = y.

  Proof. intros. unfold beq_dec. case (eq_dec x y); intuition. discr. Qed.

  Lemma beq_dec_refl : forall x, beq_dec x x = true.

  Proof. intro. unfold beq_dec. case (eq_dec x x); intros. refl. cong. Qed.

  Lemma beq_dec_sym : forall x y, beq_dec x y = beq_dec y x.

  Proof.
    intros. unfold beq_dec.
    case (eq_dec x y); case (eq_dec y x); intros; (refl || cong).
  Qed.

  Lemma beq_dec_trans : forall x y z,
    implb (beq_dec x y && beq_dec y z) (beq_dec x z) = true.

  Proof.
    intros. unfold beq_dec.
    case (eq_dec x y); case (eq_dec y z); case (eq_dec x z);
      intros; (refl || (cong || idtac)).
  Qed.

  Lemma beq_dec_ko : forall x y, beq_dec x y = false <-> x <> y.

  Proof.
    intros. case (eq_dec x y); case_eq (beq_dec x y); intuition.
    subst y. rewrite beq_dec_refl in H. discr.
    rewrite beq_dec_ok in H. contr.
  Qed.

End eq_dec.

author: sorinica

repo: spike-prover

save_path: github-repos/coq/sorinica-spike-prover


text:
(** * Testcases for [we_show_both_statements.v]
Authors:
    - Cosmin Manea (1298542)
Creation date: 22 May 2021

Test cases for the [We show/prove both directions] tactic.
Tests pass if they can be run without unhandled errors.
--------------------------------------------------------------------------------

This file is part of Waterproof-lib.

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

Waterproof-lib 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 Waterproof-lib.  If not, see <https://www.gnu.org/licenses/>.
*)

From Ltac2 Require Import Ltac2.

Load we_show_both_statements.
Require Import Waterproof.test_auxiliary.

(** Test 0: This should work *)
Goal forall n : nat, ((n = n) /\ (n + 1 = n + 1)).
Proof.
    intro n.
    We show both statements.
    - We need to show (n = n).
      reflexivity.
    - We need to show (n+1 = n+1).
      reflexivity.
Qed.

(** Test 1: This should also work *)
Goal forall n : nat, ((n = n) /\ (n + 1 = n + 1)).
Proof.
    intro n.
    We prove both statements.
    - We need to show (n = n).
      reflexivity.
    - We need to show (n+1 = n+1).
    reflexivity.
Qed.

(** Test 2: This should raise an error, because the goal is not a  *)
Goal forall n : nat, n <= n.
Proof.
    assert_raises_error (fun() => We show both statements).
Abort.

(** Test 3: This should also work *)
Goal forall n : nat, ((n = n) /\ (n + 1 = n + 1)).
Proof.
    intro n.
    We show both (n = n) and (n + 1 = n + 1).
    reflexivity.
    reflexivity.
Qed.

(** Test 4: This should also work just fine, the order has to be swapped. *)
Goal forall n : nat, ((n = n) /\ (n + 1 = n + 1)).
Proof.
    intro n.
    We show both (n + 1 = n + 1) and (n = n).
    reflexivity.
    reflexivity.
Qed.

(** Test 5: This should print that the second statement is not what is needed to be shown *)
Goal forall n : nat, ((n = n) /\ (n + 1 = n + 1)).
Proof.
    intro n.
    Fail We show both (n = n) and (n + 2 = n + 2).
Abort.

(** Test 6: This should print that the first statement is not what is needed to be shown *)
Goal forall n : nat, ((n = n) /\ (n + 1 = n + 1)).
Proof.
    intro n.
    Fail We show both (n + 2 = n + 2) and (n + 1 = n + 1).
Abort.

(** Test 7: This should print that one of the statements is not what is needed to be shown *)
Goal forall n : nat, ((n = n) /\ (n + 1 = n + 1)).
Proof.
    intro n.
    Fail We show both (n + 2 = n + 2) and (n = n).
Abort.

(** Test 8: This should raise an error: that none of the statemets are what is needed to be shown *)
Goal forall n : nat, ((n = n) /\ (n + 1 = n + 1)).
Proof.
    intro n.
    assert_raises_error (fun () => We show both (n + 2 = n + 2) and (n +3 = n + 3)).
Abort.

author: impermeable

repo: coq-waterproof