Add back equalities

2 files changed, 117 insertions, 126 deletions

diff --git a/lit/scheduling.org b/lit/scheduling.org
index c3fb12a..728dfc5 100644
--- a/lit/scheduling.org
+++ b/lit/scheduling.org
@@ -1572,7 +1572,123 @@ Require Import vericert.hls.RTLBlock.
 
 #+name: rtlblockgen-equalities-insert
 #+begin_src coq
-<<rtlblockgen-equalities>>
+Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}.
+Proof.
+  decide equality.
+Defined.
+
+Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}.
+Proof.
+  generalize comparison_eq; intro.
+  generalize Int.eq_dec; intro.
+  generalize Int64.eq_dec; intro.
+  decide equality.
+Defined.
+
+Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}.
+Proof.
+  generalize Int.eq_dec; intro.
+  generalize AST.ident_eq; intro.
+  generalize Z.eq_dec; intro.
+  generalize Ptrofs.eq_dec; intro.
+  decide equality.
+Defined.
+
+Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}.
+Proof.
+  decide equality.
+Defined.
+
+Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}.
+Proof.
+  generalize Int.eq_dec; intro.
+  generalize Int64.eq_dec; intro.
+  generalize Float.eq_dec; intro.
+  generalize Float32.eq_dec; intro.
+  generalize AST.ident_eq; intro.
+  generalize condition_eq; intro.
+  generalize addressing_eq; intro.
+  generalize typ_eq; intro.
+  decide equality.
+Defined.
+
+Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}.
+Proof.
+  decide equality.
+Defined.
+
+Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}.
+Proof.
+  generalize typ_eq; intro.
+  decide equality.
+Defined.
+
+Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}.
+Proof.
+  generalize typ_eq; intro.
+  decide equality.
+Defined.
+
+Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}.
+Proof.
+  repeat decide equality.
+Defined.
+
+Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}.
+Proof.
+  generalize operation_eq; intro.
+  decide equality.
+Defined.
+
+Lemma list_pos_eq : forall (x y : list positive), {x = y} + {x <> y}.
+Proof.
+  generalize Pos.eq_dec; intros.
+  decide equality.
+Defined.
+
+Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}.
+Proof.
+  repeat decide equality.
+Defined.
+
+Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}.
+Proof.
+  generalize Pos.eq_dec; intro.
+  generalize typ_eq; intro.
+  generalize Int.eq_dec; intro.
+  generalize memory_chunk_eq; intro.
+  generalize addressing_eq; intro.
+  generalize operation_eq; intro.
+  generalize condition_eq; intro.
+  generalize signature_eq; intro.
+  generalize list_operation_eq; intro.
+  generalize list_pos_eq; intro.
+  generalize AST.ident_eq; intro.
+  repeat decide equality.
+Defined.
+
+Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}.
+Proof.
+  generalize Pos.eq_dec; intro.
+  generalize typ_eq; intro.
+  generalize Int.eq_dec; intro.
+  generalize Int64.eq_dec; intro.
+  generalize Float.eq_dec; intro.
+  generalize Float32.eq_dec; intro.
+  generalize Ptrofs.eq_dec; intro.
+  generalize memory_chunk_eq; intro.
+  generalize addressing_eq; intro.
+  generalize operation_eq; intro.
+  generalize condition_eq; intro.
+  generalize signature_eq; intro.
+  generalize list_operation_eq; intro.
+  generalize list_pos_eq; intro.
+  generalize AST.ident_eq; intro.
+  repeat decide equality.
+Defined.
+
+Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool :=
+  if eqd a b then true else false.
 #+end_src
 
 #+name: rtlblockgen-main
@@ -1717,129 +1833,6 @@ Definition transl_program : RTL.program -> Errors.res program :=
   transform_partial_program transl_fundef.
 #+end_src
 
-** Equalities (rtlblockgen-equalities)
-
-#+name: rtlblockgen-equalities
-#+begin_src coq :tangle no
-Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}.
-Proof.
-  decide equality.
-Defined.
-
-Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}.
-Proof.
-  generalize comparison_eq; intro.
-  generalize Int.eq_dec; intro.
-  generalize Int64.eq_dec; intro.
-  decide equality.
-Defined.
-
-Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}.
-Proof.
-  generalize Int.eq_dec; intro.
-  generalize AST.ident_eq; intro.
-  generalize Z.eq_dec; intro.
-  generalize Ptrofs.eq_dec; intro.
-  decide equality.
-Defined.
-
-Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}.
-Proof.
-  decide equality.
-Defined.
-
-Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}.
-Proof.
-  generalize Int.eq_dec; intro.
-  generalize Int64.eq_dec; intro.
-  generalize Float.eq_dec; intro.
-  generalize Float32.eq_dec; intro.
-  generalize AST.ident_eq; intro.
-  generalize condition_eq; intro.
-  generalize addressing_eq; intro.
-  generalize typ_eq; intro.
-  decide equality.
-Defined.
-
-Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}.
-Proof.
-  decide equality.
-Defined.
-
-Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}.
-Proof.
-  generalize typ_eq; intro.
-  decide equality.
-Defined.
-
-Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}.
-Proof.
-  generalize typ_eq; intro.
-  decide equality.
-Defined.
-
-Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}.
-Proof.
-  repeat decide equality.
-Defined.
-
-Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}.
-Proof.
-  generalize operation_eq; intro.
-  decide equality.
-Defined.
-
-Lemma list_pos_eq : forall (x y : list positive), {x = y} + {x <> y}.
-Proof.
-  generalize Pos.eq_dec; intros.
-  decide equality.
-Defined.
-
-Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}.
-Proof.
-  repeat decide equality.
-Defined.
-
-Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}.
-Proof.
-  generalize Pos.eq_dec; intro.
-  generalize typ_eq; intro.
-  generalize Int.eq_dec; intro.
-  generalize memory_chunk_eq; intro.
-  generalize addressing_eq; intro.
-  generalize operation_eq; intro.
-  generalize condition_eq; intro.
-  generalize signature_eq; intro.
-  generalize list_operation_eq; intro.
-  generalize list_pos_eq; intro.
-  generalize AST.ident_eq; intro.
-  repeat decide equality.
-Defined.
-
-Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}.
-Proof.
-  generalize Pos.eq_dec; intro.
-  generalize typ_eq; intro.
-  generalize Int.eq_dec; intro.
-  generalize Int64.eq_dec; intro.
-  generalize Float.eq_dec; intro.
-  generalize Float32.eq_dec; intro.
-  generalize Ptrofs.eq_dec; intro.
-  generalize memory_chunk_eq; intro.
-  generalize addressing_eq; intro.
-  generalize operation_eq; intro.
-  generalize condition_eq; intro.
-  generalize signature_eq; intro.
-  generalize list_operation_eq; intro.
-  generalize list_pos_eq; intro.
-  generalize AST.ident_eq; intro.
-  repeat decide equality.
-Defined.
-
-Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool :=
-  if eqd a b then true else false.
-#+end_src
-
 * RTLBlockgenproof
 :PROPERTIES:
 :header-args:coq: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/RTLBlockgenproof.v
diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v
index 706cb09..fa462e7 100644
--- a/src/hls/RTLBlockgen.v
+++ b/src/hls/RTLBlockgen.v
@@ -31,7 +31,6 @@ Require Import vericert.hls.RTLBlock.
 (* rtlblockgen-imports ends here *)
 
 (* [[file:../../lit/scheduling.org::rtlblockgen-equalities-insert][rtlblockgen-equalities-insert]] *)
-(* [[[[file:~/projects/vericert/lit/scheduling.org::rtlblockgen-equalities][rtlblockgen-equalities]]][rtlblockgen-equalities]] *)
 Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}.
 Proof.
   decide equality.
@@ -149,7 +148,6 @@ Defined.
 
 Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool :=
   if eqd a b then true else false.
-(* rtlblockgen-equalities ends here *)
 (* rtlblockgen-equalities-insert ends here *)
 
 (* [[file:../../lit/scheduling.org::rtlblockgen-main][rtlblockgen-main]] *)