Fix imports in Coq modules

7 files changed, 162 insertions, 116 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index ce36d5b..0578f57 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -36,49 +36,39 @@ Imports
 We first need to import all of the modules that are used in the correctness proof, which includes all of the passes that are performed in Vericert and the CompCert front end.
 |*)
 
-From vericert Require Import HTLgenproof.
-
-From compcert.common Require Import
-    Errors
-    Linking.
-
-From compcert.lib Require Import
-    Coqlib.
-
-From compcert.backend Require
-    Selection
-    RTL
-    RTLgen
-    Tailcall
-    Inlining
-    Renumber
-    Constprop
-    CSE
-    Deadcode
-    Unusedglob.
-
-From compcert.cfrontend Require
-    Csyntax
-    SimplExpr
-    SimplLocals
-    Cshmgen
-    Cminorgen.
-
-From compcert.driver Require
-    Compiler.
-
-From vericert Require
-     Verilog
-     Veriloggen
-     Veriloggenproof
-     HTLgen
-     RTLBlock
-     RTLBlockgen
-     RTLPargen
-     HTLPargen
-     Pipeline.
-
-From compcert Require Import Smallstep.
+Require compcert.backend.Selection.
+Require compcert.backend.RTL.
+Require compcert.backend.RTLgen.
+Require compcert.backend.Tailcall.
+Require compcert.backend.Inlining.
+Require compcert.backend.Renumber.
+Require compcert.backend.Constprop.
+Require compcert.backend.CSE.
+Require compcert.backend.Deadcode.
+Require compcert.backend.Unusedglob.
+Require compcert.cfrontend.Csyntax.
+Require compcert.cfrontend.SimplExpr.
+Require compcert.cfrontend.SimplLocals.
+Require compcert.cfrontend.Cshmgen.
+Require compcert.cfrontend.Cminorgen.
+Require compcert.driver.Compiler.
+
+Require Import compcert.common.Errors.
+Require Import compcert.common.Linking.
+Require Import compcert.common.Smallstep.
+Require Import compcert.lib.Coqlib.
+
+Require vericert.hls.Verilog.
+Require vericert.hls.Veriloggen.
+Require vericert.hls.Veriloggenproof.
+Require vericert.hls.HTLgen.
+Require vericert.hls.RTLBlock.
+Require vericert.hls.RTLBlockgen.
+Require vericert.hls.RTLPargen.
+Require vericert.hls.HTLPargen.
+Require vericert.hls.Pipeline.
+
+Require Import vericert.hls.HTLgenproof.
 
 (*|
 Declarations
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
index d36fcee..2b6cded 100644
--- a/src/common/IntegerExtra.v
+++ b/src/common/IntegerExtra.v
@@ -17,13 +17,14 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-Require Import BinInt.
-Require Import Lia.
-Require Import ZBinary.
+Require Import Coq.ZArith.BinInt.
+Require Import Coq.micromega.Lia.
+Require Import Coq.Numbers.Integer.Binary.ZBinary.
 
-From compcert Require Import Integers Coqlib.
+Require Import compcert.lib.Coqlib.
+Require Import compcert.lib.Integers.
 
-Require Import Vericertlib.
+Require Import vericert.common.Vericertlib.
 
 Local Open Scope Z_scope.
 
@@ -337,7 +338,7 @@ Module IntExtra.
     assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
     fold (testbit (shru n (repr Byte.zwordsize)) i). rewrite bits_shru.
     change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize.
-    apply zlt_true. omega. omega.
+    apply zlt_true. lia. lia.
   Qed.
 
   Lemma bits_byte3:
@@ -347,7 +348,7 @@ Module IntExtra.
     assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
     fold (testbit (shru n (repr (2 * Byte.zwordsize))) i). rewrite bits_shru.
     change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize).
-    apply zlt_true. omega. omega.
+    apply zlt_true. lia. lia.
   Qed.
 
   Lemma bits_byte4:
@@ -357,7 +358,7 @@ Module IntExtra.
     assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
     fold (testbit (shru n (repr (3 * Byte.zwordsize))) i). rewrite bits_shru.
     change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize).
-    apply zlt_true. omega. omega.
+    apply zlt_true. lia. lia.
   Qed.
 
   Lemma bits_ofwords:
diff --git a/src/common/Maps.v b/src/common/Maps.v
index 696c9b8..f0f264d 100644
--- a/src/common/Maps.v
+++ b/src/common/Maps.v
@@ -17,13 +17,15 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From vericert Require Import Vericertlib.
+Set Implicit Arguments.
 
-From compcert Require Export Maps.
-From compcert Require Import Errors.
-Import PTree.
+Require Export compcert.lib.Maps.
 
-Set Implicit Arguments.
+Require Import compcert.common.Errors.
+
+Require Import vericert.common.Vericertlib.
+
+Import PTree.
 
 Local Open Scope error_monad_scope.
 
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index d9176db..4f6c6fa 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -1,6 +1,7 @@
 (*
  * Vericert: Verified high-level synthesis.
- * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
+ * Copyright (C) 2019-2021 Yann Herklotz <yann@yannherklotz.com>
+ *               2020 James Pollard <j@mes.dev>
  *
  * This program is free software: you can redistribute it and/or modify
  * it under the terms of the GNU General Public License as published by
@@ -16,21 +17,23 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From Coq Require Export
-     String
-     ZArith
-     Znumtheory
-     List
-     Bool.
+Set Implicit Arguments.
 
-Require Import Lia.
+Require Export Coq.Bool.Bool.
+Require Export Coq.Lists.List.
+Require Export Coq.Strings.String.
+Require Export Coq.ZArith.ZArith.
+Require Export Coq.ZArith.Znumtheory.
+Require Import Coq.micromega.Lia.
 
-From vericert Require Import Show.
+Require Export compcert.lib.Coqlib.
+Require Import compcert.lib.Integers.
+
+Require Export vericert.common.VericertTactics.
+Require Import vericert.common.Show.
 
 (* Depend on CompCert for the basic library, as they declare and prove some
    useful theorems. *)
-From compcert.lib Require Export Coqlib.
-From compcert Require Import Integers.
 
 Local Open Scope Z_scope.
 
@@ -70,7 +73,9 @@ Ltac solve_by_invert := solve_by_inverts 1.
 Ltac invert x := inversion x; subst; clear x.
 
 Ltac destruct_match :=
-  match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x end.
+  match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:? end.
+
+Ltac auto_destruct x := destruct_with_eqn x; simpl in *; try discriminate; try congruence.
 
 Ltac nicify_hypotheses :=
   repeat match goal with
@@ -180,7 +185,8 @@ Ltac liapp :=
          | _ => idtac
          end.
 
-Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; try assumption.
+Ltac crush := simplify; try discriminate; try congruence; try lia; liapp;
+              try assumption; try (solve [auto]).
 
 Global Opaque Nat.div.
 Global Opaque Z.mul.
diff --git a/src/hls/Array.v b/src/hls/Array.v
index 5c7ebc7..dec1335 100644
--- a/src/hls/Array.v
+++ b/src/hls/Array.v
@@ -18,9 +18,11 @@
 
 Set Implicit Arguments.
 
-Require Import Lia.
-Require Import Vericertlib.
-From Coq Require Import Lists.List Datatypes.
+Require Import Coq.Init.Datatypes.
+Require Import Coq.Lists.List.
+Require Import Coq.micromega.Lia.
+
+Require Import vericert.common.Vericertlib.
 
 Import ListNotations.
 
@@ -74,7 +76,7 @@ Lemma array_set_wf {A : Type} :
 Proof.
   induction l; intros; destruct i; auto.
 
-  invert H; crush; auto.
+  invert H; crush.
 Qed.
 
 Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) :=
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 474dfef..70c0454 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -16,11 +16,21 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require Errors Globalenvs Integers.
-From compcert Require Import Maps AST.
-From vericert Require Import Verilog RTLPar HTL Vericertlib AssocMap ValueInt Statemonad.
-
-Import Lia.
+Require Import Coq.micromega.Lia.
+
+Require Import compcert.common.AST.
+Require compcert.common.Errors.
+Require compcert.common.Globalenvs.
+Require compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.common.Statemonad.
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.Verilog.
+Require Import vericert.hls.RTLPar.
+Require Import vericert.hls.HTL.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.ValueInt.
 
 Hint Resolve AssocMap.gempty : htlh.
 Hint Resolve AssocMap.gso : htlh.
diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v
index 7057ce8..7c22995 100644
--- a/src/hls/Scheduleoracle.v
+++ b/src/hls/Scheduleoracle.v
@@ -20,9 +20,18 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-Require Import Globalenvs Values Integers Floats Maps.
-Require RTLBlock RTLPar Op Memory AST Registers.
-Require Import Vericertlib.
+Require compcert.backend.Registers.
+Require compcert.common.AST.
+Require Import compcert.common.Globalenvs.
+Require compcert.common.Memory.
+Require Import compcert.common.Values.
+Require Import compcert.lib.Floats.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+Require compcert.verilog.Op.
+Require vericert.hls.RTLBlock.
+Require vericert.hls.RTLPar.
+Require Import vericert.common.Vericertlib.
 
 (*|
 Schedule Oracle
@@ -154,9 +163,7 @@ Module R_indexed.
     end.
 
   Lemma index_inj:  forall (x y: t), index x = index y -> x = y.
-  Proof.
-    destruct x; destruct y; intro; try (simpl in *; congruence).
-  Qed.
+  Proof. destruct x; destruct y; crush. Qed.
 
   Definition eq := resource_eq.
 End R_indexed.
@@ -309,7 +316,7 @@ Scheme expression_ind2 := Induction for expression Sort Prop
 Lemma beq_expression_correct:
   forall e1 e2, beq_expression e1 e2 = true -> e1 = e2.
 Proof.
-  intro e1.
+  intro e1;
   apply expression_ind2 with
       (P := fun (e1 : expression) =>
             forall e2, beq_expression e1 e2 = true -> e1 = e2)
@@ -332,65 +339,93 @@ Definition check := Rtree.beq beq_expression.
 Lemma check_correct: forall (fa fb : forest) (x : resource),
   check fa fb = true -> (forall x, fa # x = fb # x).
 Proof.
-  unfold check, get_forest.
-  intros fa fb res Hbeq x.
-  pose proof Hbeq as Hbeq2.
-  pose proof (Rtree.beq_sound beq_expression fa fb) as Hsound.
-  specialize (Hsound Hbeq2 x).
-  destruct (Rtree.get x fa) eqn:?; destruct (Rtree.get x fb) eqn:?; try contradiction.
-  apply beq_expression_correct. assumption. trivial.
+  unfold check, get_forest; intros;
+  pose proof beq_expression_correct;
+  match goal with
+    [ Hbeq : context[Rtree.beq], y : Rtree.elt |- _ ] =>
+    apply (Rtree.beq_sound beq_expression fa fb) with (x := y) in Hbeq
+  end;
+  repeat destruct_match; crush.
 Qed.
 
 Lemma get_empty:
   forall r, empty#r = Ebase r.
 Proof.
-  intros r. unfold get_forest.
-  destruct (Rtree.get r empty) eqn:Heq; auto.
-  rewrite Rtree.gempty in Heq. discriminate.
+  intros; unfold get_forest;
+  destruct_match; auto; [ ];
+  match goal with
+    [ H : context[Rtree.get _ empty] |- _ ] => rewrite Rtree.gempty in H
+  end; discriminate.
+Qed.
+
+Fixpoint beq2 {A B : Type} (beqA : A -> B -> bool) (m1 : PTree.t A) (m2 : PTree.t B) {struct m1} : bool :=
+  match m1, m2 with
+  | PTree.Leaf, _ => PTree.bempty m2
+  | _, PTree.Leaf => PTree.bempty m1
+  | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 =>
+    match o1, o2 with
+    | None, None => true
+    | Some y1, Some y2 => beqA y1 y2
+    | _, _ => false
+    end
+    && beq2 beqA l1 l2 && beq2 beqA r1 r2
+  end.
+
+Lemma beq2_correct:
+  forall A B beqA m1 m2,
+    @beq2 A B beqA m1 m2 = true <->
+    (forall (x: PTree.elt),
+        match PTree.get x m1, PTree.get x m2 with
+        | None, None => True
+        | Some y1, Some y2 => beqA y1 y2 = true
+        | _, _ => False
+        end).
+Proof.
+  induction m1; intros.
+  - simpl. rewrite PTree.bempty_correct. split; intros.
+    rewrite PTree.gleaf. rewrite H. auto.
+    generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x m2); tauto.
+  - destruct m2.
+    + unfold beq2. rewrite PTree.bempty_correct. split; intros.
+      rewrite H. rewrite PTree.gleaf. auto.
+      generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x (PTree.Node m1_1 o m1_2)); tauto.
+    + simpl. split; intros.
+      * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0).
+        rewrite IHm1_1 in H3. rewrite IHm1_2 in H1.
+        destruct x; simpl. apply H1. apply H3.
+        destruct o; destruct o0; auto || congruence.
+      * apply andb_true_intro. split. apply andb_true_intro. split.
+        generalize (H xH); simpl. destruct o; destruct o0; tauto.
+        apply IHm1_1. intros; apply (H (xO x)).
+        apply IHm1_2. intros; apply (H (xI x)).
 Qed.
 
 Lemma map0:
   forall r,
   empty # r = Ebase r.
-Proof. intros. eapply get_empty. Qed.
+Proof. intros; eapply get_empty. Qed.
 
 Lemma map1:
   forall w dst dst',
   dst <> dst' ->
   (empty # dst <- w) # dst' = Ebase dst'.
-Proof.
-  intros.
-  unfold get_forest.
-  rewrite Rtree.gso. eapply map0. auto.
-Qed.
+Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply map0. Qed.
 
 Lemma genmap1:
   forall (f : forest) w dst dst',
   dst <> dst' ->
   (f # dst <- w) # dst' = f # dst'.
-Proof.
-  intros.
-  unfold get_forest.
-  rewrite Rtree.gso. reflexivity. auto.
-Qed.
+Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed.
 
 Lemma map2:
   forall (v : expression) x rs,
   (rs # x <- v) # x = v.
-Proof.
-  intros.
-  unfold get_forest.
-  rewrite Rtree.gss. trivial.
-Qed.
+Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed.
 
 Lemma tri1:
   forall x y,
   Reg x <> Reg y -> x <> y.
-Proof.
-  intros. unfold not in *; intros.
-  rewrite H0 in H. generalize (H (refl_equal (Reg y))).
-  auto.
-Qed.
+Proof. unfold not; intros; subst; auto. Qed.
 
 (*|
 Update functions.