Skip to content

Commit

Permalink
Move an instance; update imports
Browse files Browse the repository at this point in the history
  • Loading branch information
zoickx committed Sep 27, 2022
1 parent 1f75692 commit 34e0077
Show file tree
Hide file tree
Showing 3 changed files with 23 additions and 26 deletions.
26 changes: 0 additions & 26 deletions coq/DSigmaHCOL/DSigmaHCOLEval.v
Original file line number Diff line number Diff line change
Expand Up @@ -33,32 +33,6 @@ Import ListNotations.
Import MonadNotation.
Local Open Scope monad_scope.


(* Surpsingly I could not find this in Mathclasses.
Should move it somewhere *)
Instance oprod_equiv_Equivalence
`{Ae:Equiv A}
`{Be: Equiv B}
`{Aeq: Equivalence A Ae}
`{Beq: Equivalence B Be}
:
Equivalence (@prod_equiv A Ae B Be).
Proof.
split.
-
intros x.
unfold prod_equiv.
split;auto.
-
intros x y [H1 H2].
unfold prod_equiv.
split;auto.
-
intros x y z [H1 H2] [H3 H4].
unfold prod_equiv.
split;auto.
Qed.

Module Type MDSigmaHCOLEval
(Import CT : CType)
(Import NT : NType)
Expand Down
2 changes: 2 additions & 0 deletions coq/LLVMGen/Correctness_Prelude.v
Original file line number Diff line number Diff line change
Expand Up @@ -33,9 +33,11 @@ Require Export Helix.LLVMGen.Compiler.
Require Export Helix.LLVMGen.Data.
Require Export Helix.LLVMGen.Utils.
Require Export Helix.LLVMGen.Vellvm_Utils.
Require Export Helix.MSigmaHCOL.MemSetoid.
Require Export Helix.Util.OptionSetoid.
Require Export Helix.Util.ErrorSetoid.
Require Export Helix.Util.ListUtil.
Require Export Helix.Util.Misc.
Require Export Helix.Tactics.HelixTactics.

Require Export Vellvm.Utils.Tactics.
Expand Down
21 changes: 21 additions & 0 deletions coq/Util/Misc.v
Original file line number Diff line number Diff line change
Expand Up @@ -399,3 +399,24 @@ Instance R_Equiv: Equiv R := eq.

Instance R_Setoid: Setoid R.
Proof. split; auto. Qed.

Instance oprod_equiv_Equivalence
`{Ae:Equiv A}
`{Be: Equiv B}
`{Aeq: Equivalence A Ae}
`{Beq: Equivalence B Be}
:
Equivalence (@products.prod_equiv A Ae B Be).
Proof.
unfold products.prod_equiv.
split.
-
intros x.
split;auto.
-
intros x y [H1 H2].
split;auto.
-
intros x y z [H1 H2] [H3 H4].
split;auto.
Qed.

0 comments on commit 34e0077

Please sign in to comment.