From 88cef74fb9dd20ab9ddd56b6dc0099e7ad102500 Mon Sep 17 00:00:00 2001 From: Owen Conoly Date: Tue, 16 Sep 2025 12:06:33 -0400 Subject: [PATCH 1/5] remove unnecessary nth_error_flatten hyp --- src/verified_lowering/proof/Meshgrid.v | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/verified_lowering/proof/Meshgrid.v b/src/verified_lowering/proof/Meshgrid.v index 27a5d12..e1fd802 100644 --- a/src/verified_lowering/proof/Meshgrid.v +++ b/src/verified_lowering/proof/Meshgrid.v @@ -1135,10 +1135,9 @@ Proof. reflexivity. Qed. -Lemma nth_error_flatten : forall l n m xs z z0 x, +Lemma nth_error_flatten : forall l n m xs z z0, (0 <= z)%Z -> (z < Z.of_nat n)%Z -> - In x (mesh_grid (map Z.of_nat xs)) -> (0 <= z0)%Z -> (z0 < Z.of_nat m)%Z -> result_has_shape (V l) (n::m::xs) -> @@ -1147,11 +1146,11 @@ Lemma nth_error_flatten : forall l n m xs z z0 x, | Some (V v) => nth_error v (Z.to_nat z0) | _ => None end. -Proof. + Proof. induct l; intros. - - invert H4. simpl in *. lia. - - invert H4. cases a. invert H10. - assert (z = 0 \/ 0 < z)%Z by lia. invert H4. + - invert H3. simpl in *. lia. + - invert H3. cases a. invert H9. + assert (z = 0 \/ 0 < z)%Z by lia. invert H3. + simpl. rewrite nth_error_app1. 2: erewrite result_has_shape_length by eassumption; lia. reflexivity. @@ -1181,9 +1180,9 @@ Proof. cases l. rewrite nth_error_empty. simpl. rewrite nth_error_empty. auto. erewrite IHl. 4: eassumption. rewrite Nat2Z.id. auto. lia. - 4: { econstructor. reflexivity. invert H11. auto. - invert H11. auto. } - simpl in *. lia. lia. lia. + 3: { econstructor. reflexivity. invert H10. eassumption. + invert H10. auto. } + simpl in *. lia. lia. Qed. Lemma result_lookup_Z_option_flatten : forall l n m xs z z0 x, From 5a9df5d803a0a2112aefed7083ff578b7621a0c5 Mon Sep 17 00:00:00 2001 From: Owen Conoly Date: Tue, 16 Sep 2025 14:39:53 -0400 Subject: [PATCH 2/5] helpful induction scheme for results --- src/verified_lowering/proof/Result.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/verified_lowering/proof/Result.v b/src/verified_lowering/proof/Result.v index d7f25c5..2d232b5 100644 --- a/src/verified_lowering/proof/Result.v +++ b/src/verified_lowering/proof/Result.v @@ -42,9 +42,33 @@ Inductive scalar_result := | SS (r: R) | SX. +Unset Elimination Schemes. Inductive result := | S (z : scalar_result) | V (v : list result). +Set Elimination Schemes. + +Local Fixpoint result_sz (r : result) := + match r with + | Result.S _ => O + | V v => Datatypes.S (fold_right Nat.max O (map result_sz v)) + end. + +Lemma result_ind P : + (forall z, P (Result.S z)) -> + (forall v, Forall P v -> P (V v)) -> + forall r, P r. +Proof. + intros * H1 H2 r. remember (result_sz r) as sz eqn:E. + assert (Hr: (result_sz r < Datatypes.S sz)%nat) by lia. + clear E. revert r Hr. induction (Datatypes.S sz); intros. + - lia. + - destruct r; auto. apply H2. induction v. + + constructor. + + constructor. + -- apply IHn. simpl in Hr. lia. + -- apply IHv. simpl in Hr. simpl. lia. +Qed. Inductive result_has_shape : result -> list nat -> Prop := | ScalarShape : forall s, result_has_shape (S s) [] From 3a4c49b2c544261762bc3f50d0cf88303f10b2bb Mon Sep 17 00:00:00 2001 From: Owen Conoly Date: Thu, 25 Sep 2025 15:59:40 -0400 Subject: [PATCH 3/5] find . -type f | xargs sed -i 's/From Coq/From Stdlib/g' --- src/examples/Blur.v | 10 +++---- src/examples/Convolution.v | 18 ++++++------ src/examples/GatherScatter.v | 18 ++++++------ src/examples/Im2col.v | 18 ++++++------ src/examples/Matmul.v | 18 ++++++------ src/examples/TensorAdd.v | 18 ++++++------ src/verified_lowering/count_reshape/Count.v | 26 ++++++++--------- src/verified_lowering/inferpad/InferPad.v | 22 +++++++-------- src/verified_lowering/inferpad/Reify.v | 26 ++++++++--------- .../inferpad/ReifyExamples.v | 26 ++++++++--------- src/verified_lowering/proof/ATLDeep.v | 22 +++++++-------- src/verified_lowering/proof/Array.v | 22 +++++++-------- .../proof/AssignNoOverwrite.v | 22 +++++++-------- src/verified_lowering/proof/Bexpr.v | 8 +++--- src/verified_lowering/proof/Constant.v | 22 +++++++-------- src/verified_lowering/proof/ContextsAgree.v | 22 +++++++-------- src/verified_lowering/proof/Correct.v | 22 +++++++-------- src/verified_lowering/proof/InferPad.v | 22 +++++++-------- src/verified_lowering/proof/Injective.v | 10 +++---- .../proof/InterpretReindexer.v | 22 +++++++-------- src/verified_lowering/proof/ListMisc.v | 22 +++++++-------- src/verified_lowering/proof/LowerCorrect.v | 22 +++++++-------- src/verified_lowering/proof/LowerExists.v | 22 +++++++-------- src/verified_lowering/proof/Meshgrid.v | 18 ++++++------ src/verified_lowering/proof/Overflow.v | 24 ++++++++-------- src/verified_lowering/proof/Pad.v | 22 +++++++-------- src/verified_lowering/proof/Range.v | 22 +++++++-------- src/verified_lowering/proof/Result.v | 18 ++++++------ .../proof/ResultToArrayDelta.v | 22 +++++++-------- src/verified_lowering/proof/Sexpr.v | 20 ++++++------- src/verified_lowering/proof/VarGeneration.v | 10 +++---- .../proof/WellFormedAllocation.v | 22 +++++++-------- .../proof/WellFormedEnvironment.v | 22 +++++++-------- .../proof/WellFormedReindexer.v | 22 +++++++-------- src/verified_lowering/proof/Zexpr.v | 16 +++++------ src/verified_lowering/stringify/GenLib.v | 26 ++++++++--------- src/verified_lowering/stringify/GenTest.v | 22 +++++++-------- src/verified_lowering/stringify/Stringify.v | 26 ++++++++--------- src/verified_scheduling/atl/ATL.v | 18 ++++++------ src/verified_scheduling/atl/Common.v | 28 +++++++++---------- src/verified_scheduling/atl/CommonTactics.v | 28 +++++++++---------- src/verified_scheduling/atl/Div.v | 26 ++++++++--------- src/verified_scheduling/atl/GenPushout.v | 16 +++++------ src/verified_scheduling/atl/LetLifting.v | 18 ++++++------ src/verified_scheduling/atl/PairElimination.v | 16 +++++------ src/verified_scheduling/atl/Reshape.v | 28 +++++++++---------- src/verified_scheduling/atl/Tactics.v | 16 +++++------ src/verified_scheduling/atl/Var.v | 2 +- src/verified_scheduling/c/GenLib.v | 26 ++++++++--------- src/verified_scheduling/c/GenTest.v | 22 +++++++-------- src/verified_scheduling/codegen/CheckSafe.v | 22 +++++++-------- src/verified_scheduling/codegen/CodeGen.v | 22 +++++++-------- src/verified_scheduling/codegen/IntToString.v | 8 +++--- src/verified_scheduling/codegen/NatToString.v | 2 +- src/verified_scheduling/codegen/Normalize.v | 24 ++++++++-------- 55 files changed, 547 insertions(+), 547 deletions(-) diff --git a/src/examples/Blur.v b/src/examples/Blur.v index b348ac7..68884a1 100644 --- a/src/examples/Blur.v +++ b/src/examples/Blur.v @@ -1,8 +1,8 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Bool.Bool. -From Coq Require Import micromega.Lia. -From Coq Require Import Lists.List. -From Coq Require Import Reals.Reals. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Reals.Reals. Require Coq.derive.Derive. Import ListNotations. diff --git a/src/examples/Convolution.v b/src/examples/Convolution.v index 8dccb35..2d68af1 100644 --- a/src/examples/Convolution.v +++ b/src/examples/Convolution.v @@ -1,12 +1,12 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Bool.Bool. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import micromega.Lia. -From Coq Require Import Lists.List. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Int. Import Znat. -From Coq Require Import Setoids.Setoid. -From Coq Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Int. Import Znat. +From Stdlib Require Import Setoids.Setoid. +From Stdlib Require Import Logic.FunctionalExtensionality. Require Coq.derive.Derive. Import ListNotations. diff --git a/src/examples/GatherScatter.v b/src/examples/GatherScatter.v index 39139bb..5dba7df 100644 --- a/src/examples/GatherScatter.v +++ b/src/examples/GatherScatter.v @@ -1,12 +1,12 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Bool.Bool. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import micromega.Lia. -From Coq Require Import Lists.List. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Int. Import Znat. -From Coq Require Import Setoids.Setoid. -From Coq Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Int. Import Znat. +From Stdlib Require Import Setoids.Setoid. +From Stdlib Require Import Logic.FunctionalExtensionality. Require Coq.derive.Derive. Import ListNotations. diff --git a/src/examples/Im2col.v b/src/examples/Im2col.v index fbca06f..a1c9f73 100644 --- a/src/examples/Im2col.v +++ b/src/examples/Im2col.v @@ -1,12 +1,12 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Bool.Bool. -From Coq Require Import Arith.PeanoNat. -From Coq Require Import micromega.Lia. -From Coq Require Import Lists.List. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Int. Import Znat. -From Coq Require Import Setoids.Setoid. -From Coq Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Arith.PeanoNat. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Int. Import Znat. +From Stdlib Require Import Setoids.Setoid. +From Stdlib Require Import Logic.FunctionalExtensionality. Require Coq.derive.Derive. Import ListNotations. diff --git a/src/examples/Matmul.v b/src/examples/Matmul.v index 02b570c..9198e74 100644 --- a/src/examples/Matmul.v +++ b/src/examples/Matmul.v @@ -1,12 +1,12 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Bool.Bool. -From Coq Require Import Arith.PeanoNat. -From Coq Require Import micromega.Lia. -From Coq Require Import Lists.List. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Int. Import Znat. -From Coq Require Import Setoids.Setoid. -From Coq Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Arith.PeanoNat. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Int. Import Znat. +From Stdlib Require Import Setoids.Setoid. +From Stdlib Require Import Logic.FunctionalExtensionality. Require Coq.derive.Derive. Import ListNotations. diff --git a/src/examples/TensorAdd.v b/src/examples/TensorAdd.v index 1e764e3..2afa53f 100644 --- a/src/examples/TensorAdd.v +++ b/src/examples/TensorAdd.v @@ -1,12 +1,12 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Bool.Bool. -From Coq Require Import Arith.PeanoNat. -From Coq Require Import micromega.Lia. -From Coq Require Import Lists.List. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Int. Import Znat. -From Coq Require Import Setoids.Setoid. -From Coq Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Arith.PeanoNat. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Int. Import Znat. +From Stdlib Require Import Setoids.Setoid. +From Stdlib Require Import Logic.FunctionalExtensionality. Require Coq.derive.Derive. Import ListNotations. diff --git a/src/verified_lowering/count_reshape/Count.v b/src/verified_lowering/count_reshape/Count.v index 526f84e..83727f3 100644 --- a/src/verified_lowering/count_reshape/Count.v +++ b/src/verified_lowering/count_reshape/Count.v @@ -1,16 +1,16 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. -From Coq Require Import Reals.Rpower. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import Reals.Rpower. Import ListNotations. diff --git a/src/verified_lowering/inferpad/InferPad.v b/src/verified_lowering/inferpad/InferPad.v index ec79268..0ae4dc9 100644 --- a/src/verified_lowering/inferpad/InferPad.v +++ b/src/verified_lowering/inferpad/InferPad.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/inferpad/Reify.v b/src/verified_lowering/inferpad/Reify.v index b1dd31a..860ae98 100644 --- a/src/verified_lowering/inferpad/Reify.v +++ b/src/verified_lowering/inferpad/Reify.v @@ -1,16 +1,16 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. -From Coq Require Import Reals.Rpower. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import Reals.Rpower. Import ListNotations. diff --git a/src/verified_lowering/inferpad/ReifyExamples.v b/src/verified_lowering/inferpad/ReifyExamples.v index b4bb3a4..1463222 100644 --- a/src/verified_lowering/inferpad/ReifyExamples.v +++ b/src/verified_lowering/inferpad/ReifyExamples.v @@ -1,16 +1,16 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import micromega.Lia. -From Coq Require Import micromega.Zify. -From Coq Require Import Lists.List. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import micromega.Zify. +From Stdlib Require Import Lists.List. Import ListNotations. diff --git a/src/verified_lowering/proof/ATLDeep.v b/src/verified_lowering/proof/ATLDeep.v index 63ea5c8..66981dd 100644 --- a/src/verified_lowering/proof/ATLDeep.v +++ b/src/verified_lowering/proof/ATLDeep.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/Array.v b/src/verified_lowering/proof/Array.v index a021ba7..d073f54 100644 --- a/src/verified_lowering/proof/Array.v +++ b/src/verified_lowering/proof/Array.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. diff --git a/src/verified_lowering/proof/AssignNoOverwrite.v b/src/verified_lowering/proof/AssignNoOverwrite.v index db487b8..100a88b 100644 --- a/src/verified_lowering/proof/AssignNoOverwrite.v +++ b/src/verified_lowering/proof/AssignNoOverwrite.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/Bexpr.v b/src/verified_lowering/proof/Bexpr.v index 5a6f5dd..19945eb 100644 --- a/src/verified_lowering/proof/Bexpr.v +++ b/src/verified_lowering/proof/Bexpr.v @@ -1,7 +1,7 @@ -From Coq Require Import Bool.Bool. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. Set Warnings "-deprecate-hint-without-locality,-deprecated". From ATL Require Import FrapWithoutSets. diff --git a/src/verified_lowering/proof/Constant.v b/src/verified_lowering/proof/Constant.v index ebea05c..75e0d4c 100644 --- a/src/verified_lowering/proof/Constant.v +++ b/src/verified_lowering/proof/Constant.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Import ListNotations. Open Scope list_scope. diff --git a/src/verified_lowering/proof/ContextsAgree.v b/src/verified_lowering/proof/ContextsAgree.v index 118b86d..9774320 100644 --- a/src/verified_lowering/proof/ContextsAgree.v +++ b/src/verified_lowering/proof/ContextsAgree.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/Correct.v b/src/verified_lowering/proof/Correct.v index e84acae..93a90ba 100644 --- a/src/verified_lowering/proof/Correct.v +++ b/src/verified_lowering/proof/Correct.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/InferPad.v b/src/verified_lowering/proof/InferPad.v index 73dbd41..35443dc 100644 --- a/src/verified_lowering/proof/InferPad.v +++ b/src/verified_lowering/proof/InferPad.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/Injective.v b/src/verified_lowering/proof/Injective.v index ed9f520..09df85f 100644 --- a/src/verified_lowering/proof/Injective.v +++ b/src/verified_lowering/proof/Injective.v @@ -1,9 +1,9 @@ -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. Require Import String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Import ListNotations. diff --git a/src/verified_lowering/proof/InterpretReindexer.v b/src/verified_lowering/proof/InterpretReindexer.v index 5a278d7..833e27c 100644 --- a/src/verified_lowering/proof/InterpretReindexer.v +++ b/src/verified_lowering/proof/InterpretReindexer.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/ListMisc.v b/src/verified_lowering/proof/ListMisc.v index 16dcc7e..6e5f0b7 100644 --- a/src/verified_lowering/proof/ListMisc.v +++ b/src/verified_lowering/proof/ListMisc.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Import ListNotations. Open Scope list_scope. diff --git a/src/verified_lowering/proof/LowerCorrect.v b/src/verified_lowering/proof/LowerCorrect.v index ddaa0e1..092d817 100644 --- a/src/verified_lowering/proof/LowerCorrect.v +++ b/src/verified_lowering/proof/LowerCorrect.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/LowerExists.v b/src/verified_lowering/proof/LowerExists.v index 8a2d97b..1ad6387 100644 --- a/src/verified_lowering/proof/LowerExists.v +++ b/src/verified_lowering/proof/LowerExists.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/Meshgrid.v b/src/verified_lowering/proof/Meshgrid.v index e1fd802..c24ea70 100644 --- a/src/verified_lowering/proof/Meshgrid.v +++ b/src/verified_lowering/proof/Meshgrid.v @@ -1,12 +1,12 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/Overflow.v b/src/verified_lowering/proof/Overflow.v index fbea897..c9cf038 100644 --- a/src/verified_lowering/proof/Overflow.v +++ b/src/verified_lowering/proof/Overflow.v @@ -1,15 +1,15 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. -From Coq Require Import micromega.Zify. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import micromega.Zify. Import ListNotations. diff --git a/src/verified_lowering/proof/Pad.v b/src/verified_lowering/proof/Pad.v index 695141e..6167fce 100644 --- a/src/verified_lowering/proof/Pad.v +++ b/src/verified_lowering/proof/Pad.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/Range.v b/src/verified_lowering/proof/Range.v index e06fefb..e61c329 100644 --- a/src/verified_lowering/proof/Range.v +++ b/src/verified_lowering/proof/Range.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Import ListNotations. Open Scope list_scope. diff --git a/src/verified_lowering/proof/Result.v b/src/verified_lowering/proof/Result.v index 2d232b5..4062bc1 100644 --- a/src/verified_lowering/proof/Result.v +++ b/src/verified_lowering/proof/Result.v @@ -1,13 +1,13 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. Import ListNotations. diff --git a/src/verified_lowering/proof/ResultToArrayDelta.v b/src/verified_lowering/proof/ResultToArrayDelta.v index f1b56f8..a9dfad2 100644 --- a/src/verified_lowering/proof/ResultToArrayDelta.v +++ b/src/verified_lowering/proof/ResultToArrayDelta.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/Sexpr.v b/src/verified_lowering/proof/Sexpr.v index 738a2ba..115a3ec 100644 --- a/src/verified_lowering/proof/Sexpr.v +++ b/src/verified_lowering/proof/Sexpr.v @@ -1,15 +1,15 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. -From Coq Require Import Reals.Rpower. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import Reals.Rpower. Require Import Coq.Logic.FunctionalExtensionality. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. diff --git a/src/verified_lowering/proof/VarGeneration.v b/src/verified_lowering/proof/VarGeneration.v index d6e2223..f694b5e 100644 --- a/src/verified_lowering/proof/VarGeneration.v +++ b/src/verified_lowering/proof/VarGeneration.v @@ -1,9 +1,9 @@ -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. Require Import String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Import ListNotations. diff --git a/src/verified_lowering/proof/WellFormedAllocation.v b/src/verified_lowering/proof/WellFormedAllocation.v index 0bc1c95..60a0e43 100644 --- a/src/verified_lowering/proof/WellFormedAllocation.v +++ b/src/verified_lowering/proof/WellFormedAllocation.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/WellFormedEnvironment.v b/src/verified_lowering/proof/WellFormedEnvironment.v index dedb5c4..bea78c5 100644 --- a/src/verified_lowering/proof/WellFormedEnvironment.v +++ b/src/verified_lowering/proof/WellFormedEnvironment.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/WellFormedReindexer.v b/src/verified_lowering/proof/WellFormedReindexer.v index 0ebec8a..70b4eeb 100644 --- a/src/verified_lowering/proof/WellFormedReindexer.v +++ b/src/verified_lowering/proof/WellFormedReindexer.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/Zexpr.v b/src/verified_lowering/proof/Zexpr.v index c1c7e1e..4eb4114 100644 --- a/src/verified_lowering/proof/Zexpr.v +++ b/src/verified_lowering/proof/Zexpr.v @@ -1,11 +1,11 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. Require Import Coq.Logic.FunctionalExtensionality. diff --git a/src/verified_lowering/stringify/GenLib.v b/src/verified_lowering/stringify/GenLib.v index ad922d0..963abc6 100644 --- a/src/verified_lowering/stringify/GenLib.v +++ b/src/verified_lowering/stringify/GenLib.v @@ -1,16 +1,16 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import micromega.Lia. -From Coq Require Import micromega.Zify. -From Coq Require Import Lists.List. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import micromega.Zify. +From Stdlib Require Import Lists.List. Import ListNotations. diff --git a/src/verified_lowering/stringify/GenTest.v b/src/verified_lowering/stringify/GenTest.v index 90920c0..16a16b3 100644 --- a/src/verified_lowering/stringify/GenTest.v +++ b/src/verified_lowering/stringify/GenTest.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import Lists.List. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Lists.List. Import ListNotations. diff --git a/src/verified_lowering/stringify/Stringify.v b/src/verified_lowering/stringify/Stringify.v index ee56027..bdba753 100644 --- a/src/verified_lowering/stringify/Stringify.v +++ b/src/verified_lowering/stringify/Stringify.v @@ -1,16 +1,16 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import Lists.List. -From Coq Require Import micromega.Lia. -From Coq Require Import Reals.Rpower. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Lists.List. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import Reals.Rpower. Import ListNotations. diff --git a/src/verified_scheduling/atl/ATL.v b/src/verified_scheduling/atl/ATL.v index 60e4bb5..5f6d793 100644 --- a/src/verified_scheduling/atl/ATL.v +++ b/src/verified_scheduling/atl/ATL.v @@ -1,12 +1,12 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import micromega.Lia. -From Coq Require Import micromega.Zify. -From Coq Require Import Lists.List. -From Coq Require Import Reals.Reals. Import RIneq. Import Rdefinitions. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import micromega.Zify. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Reals.Reals. Import RIneq. Import Rdefinitions. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Logic.FunctionalExtensionality. Import ListNotations. diff --git a/src/verified_scheduling/atl/Common.v b/src/verified_scheduling/atl/Common.v index fe0edf3..721d307 100644 --- a/src/verified_scheduling/atl/Common.v +++ b/src/verified_scheduling/atl/Common.v @@ -1,17 +1,17 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import micromega.Lia. -From Coq Require Import micromega.Zify. -From Coq Require Import Lists.List. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Setoids.Setoid. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import Classes.Morphisms. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import micromega.Zify. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Setoids.Setoid. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Classes.Morphisms. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_scheduling/atl/CommonTactics.v b/src/verified_scheduling/atl/CommonTactics.v index 6214c14..7d03a95 100644 --- a/src/verified_scheduling/atl/CommonTactics.v +++ b/src/verified_scheduling/atl/CommonTactics.v @@ -1,17 +1,17 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import micromega.Lia. -From Coq Require Import micromega.Zify. -From Coq Require Import Lists.List. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Setoids.Setoid. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import Classes.Morphisms. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import micromega.Zify. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Setoids.Setoid. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Classes.Morphisms. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_scheduling/atl/Div.v b/src/verified_scheduling/atl/Div.v index ee47efb..ef72926 100644 --- a/src/verified_scheduling/atl/Div.v +++ b/src/verified_scheduling/atl/Div.v @@ -1,16 +1,16 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import micromega.Lia. -From Coq Require Import Lists.List. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Setoids.Setoid. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import Classes.Morphisms. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Setoids.Setoid. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Classes.Morphisms. From ATL Require Import Tactics FrapWithoutSets. diff --git a/src/verified_scheduling/atl/GenPushout.v b/src/verified_scheduling/atl/GenPushout.v index fa2fada..aa505df 100644 --- a/src/verified_scheduling/atl/GenPushout.v +++ b/src/verified_scheduling/atl/GenPushout.v @@ -1,11 +1,11 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import micromega.Lia. -From Coq Require Import micromega.Zify. -From Coq Require Import Lists.List. -From Coq Require Import Vectors.Vector. -From Coq Require Import Reals.Reals. Import RIneq. Import Rdefinitions. -From Coq Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import micromega.Zify. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Vectors.Vector. +From Stdlib Require Import Reals.Reals. Import RIneq. Import Rdefinitions. +From Stdlib Require Import Logic.FunctionalExtensionality. Import ListNotations. From ATL Require Import ATL Common Tactics Div CommonTactics. diff --git a/src/verified_scheduling/atl/LetLifting.v b/src/verified_scheduling/atl/LetLifting.v index f710143..8873a9c 100644 --- a/src/verified_scheduling/atl/LetLifting.v +++ b/src/verified_scheduling/atl/LetLifting.v @@ -1,12 +1,12 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import micromega.Lia. -From Coq Require Import micromega.Zify. -From Coq Require Import Lists.List. -From Coq Require Import Reals.Reals. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import Reals.Rpower. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import micromega.Zify. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Reals.Reals. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Reals.Rpower. Import ListNotations. From ATL Require Import ATL Common Tactics CommonTactics. diff --git a/src/verified_scheduling/atl/PairElimination.v b/src/verified_scheduling/atl/PairElimination.v index e31eeab..1efb091 100644 --- a/src/verified_scheduling/atl/PairElimination.v +++ b/src/verified_scheduling/atl/PairElimination.v @@ -1,11 +1,11 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import ZArith.BinInt. -From Coq Require Import micromega.Lia. -From Coq Require Import micromega.Zify. -From Coq Require Import Lists.List. -From Coq Require Import Vectors.Vector. -From Coq Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import ZArith.BinInt. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import micromega.Zify. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Vectors.Vector. +From Stdlib Require Import Logic.FunctionalExtensionality. Import ListNotations. From ATL Require Import ATL Common CommonTactics Tactics Div. diff --git a/src/verified_scheduling/atl/Reshape.v b/src/verified_scheduling/atl/Reshape.v index 89695e0..6d637c9 100644 --- a/src/verified_scheduling/atl/Reshape.v +++ b/src/verified_scheduling/atl/Reshape.v @@ -1,17 +1,17 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import micromega.Lia. -From Coq Require Import micromega.Zify. -From Coq Require Import Lists.List. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Znat. -From Coq Require Import Setoids.Setoid. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import Classes.Morphisms. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import micromega.Zify. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Setoids.Setoid. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Classes.Morphisms. Import ListNotations. From ATL Require Import ATL Tactics Common CommonTactics Div GenPushout LetLifting. diff --git a/src/verified_scheduling/atl/Tactics.v b/src/verified_scheduling/atl/Tactics.v index 91be4ee..4c25ba2 100644 --- a/src/verified_scheduling/atl/Tactics.v +++ b/src/verified_scheduling/atl/Tactics.v @@ -1,11 +1,11 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Bool.Bool. -From Coq Require Import micromega.Lia. -From Coq Require Import micromega.Zify. -From Coq Require Import Lists.List. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Int. Import Znat BinInt.Z. -From Coq Require Import Setoids.Setoid. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import micromega.Zify. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Int. Import Znat BinInt.Z. +From Stdlib Require Import Setoids.Setoid. Import ListNotations. From ATL Require Import ATL. diff --git a/src/verified_scheduling/atl/Var.v b/src/verified_scheduling/atl/Var.v index 4148f63..a007ff5 100644 --- a/src/verified_scheduling/atl/Var.v +++ b/src/verified_scheduling/atl/Var.v @@ -1,5 +1,5 @@ Require Import String. -From Coq Require Import Lists.List. +From Stdlib Require Import Lists.List. Import ListNotations. Notation var := string. diff --git a/src/verified_scheduling/c/GenLib.v b/src/verified_scheduling/c/GenLib.v index 73a58f3..ed011b0 100644 --- a/src/verified_scheduling/c/GenLib.v +++ b/src/verified_scheduling/c/GenLib.v @@ -1,16 +1,16 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import micromega.Lia. -From Coq Require Import micromega.Zify. -From Coq Require Import Lists.List. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import micromega.Zify. +From Stdlib Require Import Lists.List. Import ListNotations. diff --git a/src/verified_scheduling/c/GenTest.v b/src/verified_scheduling/c/GenTest.v index f2bc159..d616759 100644 --- a/src/verified_scheduling/c/GenTest.v +++ b/src/verified_scheduling/c/GenTest.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import Lists.List. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Lists.List. Import ListNotations. diff --git a/src/verified_scheduling/codegen/CheckSafe.v b/src/verified_scheduling/codegen/CheckSafe.v index 8e974f7..ac1bf10 100644 --- a/src/verified_scheduling/codegen/CheckSafe.v +++ b/src/verified_scheduling/codegen/CheckSafe.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import micromega.Lia. -From Coq Require Import micromega.Zify. -From Coq Require Import Lists.List. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import micromega.Zify. +From Stdlib Require Import Lists.List. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. Set Warnings "-omega-is-deprecated,-deprecated". diff --git a/src/verified_scheduling/codegen/CodeGen.v b/src/verified_scheduling/codegen/CodeGen.v index 25d147f..c6690e7 100644 --- a/src/verified_scheduling/codegen/CodeGen.v +++ b/src/verified_scheduling/codegen/CodeGen.v @@ -1,14 +1,14 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import Lists.List. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Lists.List. Import ListNotations. diff --git a/src/verified_scheduling/codegen/IntToString.v b/src/verified_scheduling/codegen/IntToString.v index af8c014..441470b 100644 --- a/src/verified_scheduling/codegen/IntToString.v +++ b/src/verified_scheduling/codegen/IntToString.v @@ -1,7 +1,7 @@ -From Coq Require Import Ascii String. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. +From Stdlib Require Import Ascii String. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. Require Import Coq.Strings.String. diff --git a/src/verified_scheduling/codegen/NatToString.v b/src/verified_scheduling/codegen/NatToString.v index a9f5ace..fb15c96 100644 --- a/src/verified_scheduling/codegen/NatToString.v +++ b/src/verified_scheduling/codegen/NatToString.v @@ -1,4 +1,4 @@ -From Coq Require Import Ascii String Arith. +From Stdlib Require Import Ascii String Arith. Require Import Coq.Strings.String. Definition nat_to_ascii (n : nat) : ascii := diff --git a/src/verified_scheduling/codegen/Normalize.v b/src/verified_scheduling/codegen/Normalize.v index 7221f8d..a9ee1bf 100644 --- a/src/verified_scheduling/codegen/Normalize.v +++ b/src/verified_scheduling/codegen/Normalize.v @@ -1,15 +1,15 @@ -From Coq Require Import Arith.Arith. -From Coq Require Import Arith.EqNat. -From Coq Require Import Arith.PeanoNat. Import Nat. -From Coq Require Import Bool.Bool. -From Coq Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -From Coq Require Import ZArith.Zdiv. -From Coq Require Import ZArith.Int. -From Coq Require Import ZArith.Znat. -From Coq Require Import Strings.String. -From Coq Require Import Logic.FunctionalExtensionality. -From Coq Require Import micromega.Lia. -From Coq Require Import micromega.Zify. +From Stdlib Require Import Arith.Arith. +From Stdlib Require Import Arith.EqNat. +From Stdlib Require Import Arith.PeanoNat. Import Nat. +From Stdlib Require Import Bool.Bool. +From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. +From Stdlib Require Import ZArith.Zdiv. +From Stdlib Require Import ZArith.Int. +From Stdlib Require Import ZArith.Znat. +From Stdlib Require Import Strings.String. +From Stdlib Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import micromega.Lia. +From Stdlib Require Import micromega.Zify. Require Import Ltac2.Ltac2. Require Import Ltac2.Option. From 7341fd2b01fe9df3d915430a9834e6af36e46e3b Mon Sep 17 00:00:00 2001 From: Owen Conoly Date: Thu, 25 Sep 2025 18:44:59 -0400 Subject: [PATCH 4/5] make it work with Rocq 9.0 (no errors or warnings due to version change) --- src/examples/Blur.v | 1 + .../inferpad/.Makefile.coq.d | 9 - src/verified_lowering/inferpad/InferPad.v | 2 +- src/verified_lowering/proof/ATLDeep.v | 8 +- .../proof/AssignNoOverwrite.v | 4 +- src/verified_lowering/proof/Constant.v | 2 +- src/verified_lowering/proof/ContextsAgree.v | 2 +- src/verified_lowering/proof/Correct.v | 4 +- src/verified_lowering/proof/InferPad.v | 2 +- src/verified_lowering/proof/Injective.v | 60 +- .../proof/InterpretReindexer.v | 24 +- src/verified_lowering/proof/ListMisc.v | 36 +- src/verified_lowering/proof/LowerCorrect.v | 32 +- src/verified_lowering/proof/LowerExists.v | 32 +- src/verified_lowering/proof/Meshgrid.v | 20 +- src/verified_lowering/proof/Pad.v | 485 ++++----- src/verified_lowering/proof/Range.v | 4 +- src/verified_lowering/proof/Result.v | 78 +- .../proof/ResultToArrayDelta.v | 12 +- src/verified_lowering/proof/Sexpr.v | 2 +- src/verified_lowering/proof/VarGeneration.v | 2 +- .../proof/WellFormedAllocation.v | 21 +- .../proof/WellFormedEnvironment.v | 2 +- .../proof/WellFormedReindexer.v | 10 +- src/verified_lowering/proof/Zexpr.v | 2 +- src/verified_scheduling/atl/.Makefile.coq.d | 48 - src/verified_scheduling/atl/ATL.v | 22 +- src/verified_scheduling/atl/Common.v | 21 +- src/verified_scheduling/atl/CommonTactics.v | 4 +- src/verified_scheduling/atl/Div.v | 18 +- src/verified_scheduling/atl/FrapWithoutSets.v | 6 +- src/verified_scheduling/atl/Map.v | 2 +- src/verified_scheduling/atl/ModelCheck.v | 3 +- src/verified_scheduling/atl/Reshape.v | 1 + src/verified_scheduling/atl/Sets.v | 4 +- src/verified_scheduling/atl/Tactics.v | 4 +- src/verified_scheduling/atl/Var.v | 3 +- .../codegen/.Makefileg.coq.d | 18 - .../codegen/IdentParsing.v | 6 +- src/verified_scheduling/codegen/IntToString.v | 4 +- src/verified_scheduling/codegen/Makefileg.coq | 989 ------------------ .../codegen/Makefileg.coq.conf | 71 -- src/verified_scheduling/codegen/NatToString.v | 2 +- 43 files changed, 440 insertions(+), 1642 deletions(-) delete mode 100644 src/verified_lowering/inferpad/.Makefile.coq.d delete mode 100644 src/verified_scheduling/atl/.Makefile.coq.d delete mode 100644 src/verified_scheduling/codegen/.Makefileg.coq.d delete mode 100644 src/verified_scheduling/codegen/Makefileg.coq delete mode 100644 src/verified_scheduling/codegen/Makefileg.coq.conf diff --git a/src/examples/Blur.v b/src/examples/Blur.v index 68884a1..5d4296a 100644 --- a/src/examples/Blur.v +++ b/src/examples/Blur.v @@ -6,6 +6,7 @@ From Stdlib Require Import Reals.Reals. Require Coq.derive.Derive. Import ListNotations. +Import Znat. From ATL Require Import ATL Common Reshape Tactics LetLifting Div GenPushout CommonTactics. diff --git a/src/verified_lowering/inferpad/.Makefile.coq.d b/src/verified_lowering/inferpad/.Makefile.coq.d deleted file mode 100644 index 347f560..0000000 --- a/src/verified_lowering/inferpad/.Makefile.coq.d +++ /dev/null @@ -1,9 +0,0 @@ -Reify.vo Reify.glob Reify.v.beautified Reify.required_vo: Reify.v ../../verified_scheduling/codegen/IdentParsing.vo ../../verified_scheduling/codegen/NatToString.vo ../../verified_scheduling/codegen/IntToString.vo ../../verified_scheduling/codegen/Normalize.vo ../../verified_scheduling/codegen/CodeGen.vo ../proof/ATLDeep.vo ../proof/Sexpr.vo ../proof/Zexpr.vo ../proof/Bexpr.vo ../../verified_scheduling/atl/ATL.vo ../../verified_scheduling/atl/Common.vo ../../verified_scheduling/atl/CommonTactics.vo ../../verified_scheduling/atl/Div.vo -Reify.vio: Reify.v ../../verified_scheduling/codegen/IdentParsing.vio ../../verified_scheduling/codegen/NatToString.vio ../../verified_scheduling/codegen/IntToString.vio ../../verified_scheduling/codegen/Normalize.vio ../../verified_scheduling/codegen/CodeGen.vio ../proof/ATLDeep.vio ../proof/Sexpr.vio ../proof/Zexpr.vio ../proof/Bexpr.vio ../../verified_scheduling/atl/ATL.vio ../../verified_scheduling/atl/Common.vio ../../verified_scheduling/atl/CommonTactics.vio ../../verified_scheduling/atl/Div.vio -Reify.vos Reify.vok Reify.required_vos: Reify.v ../../verified_scheduling/codegen/IdentParsing.vos ../../verified_scheduling/codegen/NatToString.vos ../../verified_scheduling/codegen/IntToString.vos ../../verified_scheduling/codegen/Normalize.vos ../../verified_scheduling/codegen/CodeGen.vos ../proof/ATLDeep.vos ../proof/Sexpr.vos ../proof/Zexpr.vos ../proof/Bexpr.vos ../../verified_scheduling/atl/ATL.vos ../../verified_scheduling/atl/Common.vos ../../verified_scheduling/atl/CommonTactics.vos ../../verified_scheduling/atl/Div.vos -ReifyExamples.vo ReifyExamples.glob ReifyExamples.v.beautified ReifyExamples.required_vo: ReifyExamples.v ../../verified_scheduling/atl/ATL.vo ../../verified_scheduling/atl/Tactics.vo ../../verified_scheduling/atl/Common.vo ../../verified_scheduling/atl/CommonTactics.vo ../../verified_scheduling/atl/Div.vo ../../verified_scheduling/atl/Reshape.vo ../../verified_scheduling/codegen/IdentParsing.vo ../../verified_scheduling/codegen/NatToString.vo ../../verified_scheduling/codegen/IntToString.vo ../../verified_scheduling/codegen/CodeGen.vo ../../verified_scheduling/codegen/Normalize.vo ../../verified_scheduling/codegen/CheckSafe.vo ../../examples/GatherScatter.vo ../../examples/Convolution.vo ../../examples/Im2col.vo ../../examples/Blur.vo ../../examples/TensorAdd.vo ../../examples/Matmul.vo Reify.vo ../proof/Zexpr.vo ../proof/ATLDeep.vo ../proof/Bexpr.vo ../proof/Sexpr.vo -ReifyExamples.vio: ReifyExamples.v ../../verified_scheduling/atl/ATL.vio ../../verified_scheduling/atl/Tactics.vio ../../verified_scheduling/atl/Common.vio ../../verified_scheduling/atl/CommonTactics.vio ../../verified_scheduling/atl/Div.vio ../../verified_scheduling/atl/Reshape.vio ../../verified_scheduling/codegen/IdentParsing.vio ../../verified_scheduling/codegen/NatToString.vio ../../verified_scheduling/codegen/IntToString.vio ../../verified_scheduling/codegen/CodeGen.vio ../../verified_scheduling/codegen/Normalize.vio ../../verified_scheduling/codegen/CheckSafe.vio ../../examples/GatherScatter.vio ../../examples/Convolution.vio ../../examples/Im2col.vio ../../examples/Blur.vio ../../examples/TensorAdd.vio ../../examples/Matmul.vio Reify.vio ../proof/Zexpr.vio ../proof/ATLDeep.vio ../proof/Bexpr.vio ../proof/Sexpr.vio -ReifyExamples.vos ReifyExamples.vok ReifyExamples.required_vos: ReifyExamples.v ../../verified_scheduling/atl/ATL.vos ../../verified_scheduling/atl/Tactics.vos ../../verified_scheduling/atl/Common.vos ../../verified_scheduling/atl/CommonTactics.vos ../../verified_scheduling/atl/Div.vos ../../verified_scheduling/atl/Reshape.vos ../../verified_scheduling/codegen/IdentParsing.vos ../../verified_scheduling/codegen/NatToString.vos ../../verified_scheduling/codegen/IntToString.vos ../../verified_scheduling/codegen/CodeGen.vos ../../verified_scheduling/codegen/Normalize.vos ../../verified_scheduling/codegen/CheckSafe.vos ../../examples/GatherScatter.vos ../../examples/Convolution.vos ../../examples/Im2col.vos ../../examples/Blur.vos ../../examples/TensorAdd.vos ../../examples/Matmul.vos Reify.vos ../proof/Zexpr.vos ../proof/ATLDeep.vos ../proof/Bexpr.vos ../proof/Sexpr.vos -InferPad.vo InferPad.glob InferPad.v.beautified InferPad.required_vo: InferPad.v ../../verified_scheduling/atl/ATL.vo ../../verified_scheduling/atl/Map.vo ../../verified_scheduling/atl/Sets.vo ../../verified_scheduling/atl/FrapWithoutSets.vo ../../verified_scheduling/atl/Div.vo ../../verified_scheduling/atl/Tactics.vo ../../verified_scheduling/atl/Common.vo ../../verified_scheduling/atl/CommonTactics.vo ../../examples/TensorAdd.vo ../../examples/Matmul.vo ../../examples/GatherScatter.vo ../../examples/Im2col.vo ../../examples/Convolution.vo ../../examples/Blur.vo ../proof/Zexpr.vo ../proof/Bexpr.vo ../proof/Array.vo ../proof/Range.vo ../proof/Sexpr.vo ../proof/Result.vo ../proof/ListMisc.vo ../proof/Meshgrid.vo ../proof/VarGeneration.vo ../proof/Constant.vo ../proof/ATLDeep.vo ../proof/Pad.vo Reify.vo -InferPad.vio: InferPad.v ../../verified_scheduling/atl/ATL.vio ../../verified_scheduling/atl/Map.vio ../../verified_scheduling/atl/Sets.vio ../../verified_scheduling/atl/FrapWithoutSets.vio ../../verified_scheduling/atl/Div.vio ../../verified_scheduling/atl/Tactics.vio ../../verified_scheduling/atl/Common.vio ../../verified_scheduling/atl/CommonTactics.vio ../../examples/TensorAdd.vio ../../examples/Matmul.vio ../../examples/GatherScatter.vio ../../examples/Im2col.vio ../../examples/Convolution.vio ../../examples/Blur.vio ../proof/Zexpr.vio ../proof/Bexpr.vio ../proof/Array.vio ../proof/Range.vio ../proof/Sexpr.vio ../proof/Result.vio ../proof/ListMisc.vio ../proof/Meshgrid.vio ../proof/VarGeneration.vio ../proof/Constant.vio ../proof/ATLDeep.vio ../proof/Pad.vio Reify.vio -InferPad.vos InferPad.vok InferPad.required_vos: InferPad.v ../../verified_scheduling/atl/ATL.vos ../../verified_scheduling/atl/Map.vos ../../verified_scheduling/atl/Sets.vos ../../verified_scheduling/atl/FrapWithoutSets.vos ../../verified_scheduling/atl/Div.vos ../../verified_scheduling/atl/Tactics.vos ../../verified_scheduling/atl/Common.vos ../../verified_scheduling/atl/CommonTactics.vos ../../examples/TensorAdd.vos ../../examples/Matmul.vos ../../examples/GatherScatter.vos ../../examples/Im2col.vos ../../examples/Convolution.vos ../../examples/Blur.vos ../proof/Zexpr.vos ../proof/Bexpr.vos ../proof/Array.vos ../proof/Range.vos ../proof/Sexpr.vos ../proof/Result.vos ../proof/ListMisc.vos ../proof/Meshgrid.vos ../proof/VarGeneration.vos ../proof/Constant.vos ../proof/ATLDeep.vos ../proof/Pad.vos Reify.vos diff --git a/src/verified_lowering/inferpad/InferPad.v b/src/verified_lowering/inferpad/InferPad.v index 0ae4dc9..8858f5b 100644 --- a/src/verified_lowering/inferpad/InferPad.v +++ b/src/verified_lowering/inferpad/InferPad.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. diff --git a/src/verified_lowering/proof/ATLDeep.v b/src/verified_lowering/proof/ATLDeep.v index 66981dd..6329a4b 100644 --- a/src/verified_lowering/proof/ATLDeep.v +++ b/src/verified_lowering/proof/ATLDeep.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. @@ -636,7 +636,7 @@ Hint Resolve no_dup_var_generation no_dup_mesh_grid not_var_generation_in_dom2 not_var_generation_in_index2 not_var_generation_in_index not_var_generation_in_dom : reindexers. Hint Extern 3 (Datatypes.length _ = Datatypes.length _) => - rewrite map_length; rewrite length_nat_range_rec; + rewrite length_map; rewrite length_nat_range_rec; eapply length_mesh_grid_indices; eassumption : reindexers. Lemma result_shape_gen_length : forall i lo hi body c v sh l, @@ -660,8 +660,8 @@ Proof. Qed. Hint Extern 3 (Datatypes.length (map _ _) = Datatypes.length _) => - rewrite map_length; rewrite length_nat_range_rec; -rewrite map_length; eapply length_mesh_grid_indices; eassumption : reindexers. + rewrite length_map; rewrite length_nat_range_rec; +rewrite length_map; eapply length_mesh_grid_indices; eassumption : reindexers. Lemma eq_eval_stmt_for : forall v st h st' h' body1 body2 hi lo i, diff --git a/src/verified_lowering/proof/AssignNoOverwrite.v b/src/verified_lowering/proof/AssignNoOverwrite.v index 100a88b..5d755c5 100644 --- a/src/verified_lowering/proof/AssignNoOverwrite.v +++ b/src/verified_lowering/proof/AssignNoOverwrite.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. @@ -32,7 +32,7 @@ Hint Resolve no_dup_var_generation no_dup_mesh_grid not_var_generation_in_dom2 not_var_generation_in_index2 not_var_generation_in_index not_var_generation_in_dom : reindexers. Hint Extern 3 (Datatypes.length _ = Datatypes.length _) => - rewrite map_length; rewrite length_nat_range_rec; + rewrite length_map; rewrite length_nat_range_rec; eapply length_mesh_grid_indices; eassumption : reindexers. Arguments flatten : simpl nomatch. diff --git a/src/verified_lowering/proof/Constant.v b/src/verified_lowering/proof/Constant.v index 75e0d4c..82f7a40 100644 --- a/src/verified_lowering/proof/Constant.v +++ b/src/verified_lowering/proof/Constant.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Import ListNotations. Open Scope list_scope. diff --git a/src/verified_lowering/proof/ContextsAgree.v b/src/verified_lowering/proof/ContextsAgree.v index 9774320..fa11abd 100644 --- a/src/verified_lowering/proof/ContextsAgree.v +++ b/src/verified_lowering/proof/ContextsAgree.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. diff --git a/src/verified_lowering/proof/Correct.v b/src/verified_lowering/proof/Correct.v index 93a90ba..4411cf9 100644 --- a/src/verified_lowering/proof/Correct.v +++ b/src/verified_lowering/proof/Correct.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. @@ -33,7 +33,7 @@ Hint Resolve no_dup_var_generation no_dup_mesh_grid not_var_generation_in_dom2 not_var_generation_in_index2 not_var_generation_in_index not_var_generation_in_dom : reindexers. Hint Extern 3 (Datatypes.length _ = Datatypes.length _) => - rewrite map_length; rewrite length_nat_range_rec; + rewrite length_map; rewrite length_nat_range_rec; eapply length_mesh_grid_indices; eassumption : reindexers. Arguments flatten : simpl nomatch. diff --git a/src/verified_lowering/proof/InferPad.v b/src/verified_lowering/proof/InferPad.v index 35443dc..6e02f4c 100644 --- a/src/verified_lowering/proof/InferPad.v +++ b/src/verified_lowering/proof/InferPad.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. diff --git a/src/verified_lowering/proof/Injective.v b/src/verified_lowering/proof/Injective.v index 09df85f..9bc83a0 100644 --- a/src/verified_lowering/proof/Injective.v +++ b/src/verified_lowering/proof/Injective.v @@ -1,10 +1,10 @@ From Stdlib Require Import ZArith.Zdiv. From Stdlib Require Import ZArith.Int. From Stdlib Require Import ZArith.Znat. -Require Import String. +From Stdlib Require Import String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Import ListNotations. @@ -210,7 +210,7 @@ partial_interpret_reindexer ( Z.to_nat ((eval_Zexpr_Z_total $0 n) // (eval_Zexpr_Z_total $0 k)) :: Z.to_nat (eval_Zexpr_Z_total $0 k) ::map Z.to_nat (map (eval_Zexpr_Z_total $0) l0)) 0)) v - ((z0 / eval_Zexpr_Z_total $0 k)%Z :: (Coq.ZArith.BinIntDef.Z.modulo z0 (eval_Zexpr_Z_total $0 k)) :: args1). + ((z0 / eval_Zexpr_Z_total $0 k)%Z :: (Stdlib.ZArith.BinIntDef.Z.modulo z0 (eval_Zexpr_Z_total $0 k)) :: args1). Proof. intros ? ? ? ? ? ? ? Heqk Hvar HeqZlistwrap Hvarsub Hmap Hvarrdx Hmnonneg Hknonneg Harg Hle. @@ -242,19 +242,19 @@ Proof. 2: { unfold eq_zexpr in *. invs. rewrite H2. sets. } erewrite index_to_partial_function_subst_vars. 2: { eauto with reindexers. } - 2: { rewrite map_length. rewrite map_length. + 2: { rewrite length_map. rewrite length_map. rewrite length_nat_range_rec. rewrite <- mesh_grid_filter_until in Harg. eapply length_mesh_grid_indices_Z in Harg. - rewrite map_length in Harg. lia. } + rewrite length_map in Harg. lia. } symmetry. erewrite index_to_partial_function_subst_vars. 2: { eauto with reindexers. } - 2: { rewrite map_length. rewrite map_length. + 2: { rewrite length_map. rewrite length_map. rewrite length_nat_range_rec. rewrite <- mesh_grid_filter_until in Harg. eapply length_mesh_grid_indices_Z in Harg. - rewrite map_length in Harg. lia. } + rewrite length_map in Harg. lia. } symmetry. rewrite map_fold_left_subst_var_in_Z_tup_reindexer. 2: { eauto. } @@ -273,19 +273,19 @@ Proof. 2: { simpl. invert Heqk. rewrite H0. sets. } 2: { simpl. invert Heqk. rewrite H0. sets. } rewrite map_fold_left_subst_var_in_Z_tup_shape_to_index. - 2: { rewrite map_length. rewrite map_length. + 2: { rewrite length_map. rewrite length_map. rewrite length_nat_range_rec. rewrite <- mesh_grid_filter_until in Harg. eapply length_mesh_grid_indices_Z in Harg. - rewrite map_length in Harg. lia. } + rewrite length_map in Harg. lia. } 2: { eauto with reindexers. } symmetry. rewrite map_fold_left_subst_var_in_Z_tup_combine. - 2: { rewrite map_length. rewrite map_length. + 2: { rewrite length_map. rewrite length_map. rewrite length_nat_range_rec. rewrite <- mesh_grid_filter_until in Harg. eapply length_mesh_grid_indices_Z in Harg. - rewrite map_length in Harg. lia. } + rewrite length_map in Harg. lia. } 2: { eauto with reindexers. } erewrite eq_index_to_partial_function. reflexivity. eapply eq_Z_tuple_index_list_partially_eval_Z_tup. @@ -1027,11 +1027,11 @@ Proof. erewrite index_to_partial_function_subst_vars; unfold nat_range; eauto with reindexers. - 2: rewrite map_length; rewrite length_nat_range_rec; lia. + 2: rewrite length_map; rewrite length_nat_range_rec; lia. symmetry. erewrite index_to_partial_function_subst_vars; unfold nat_range; eauto with reindexers. - 2: rewrite map_length; rewrite length_nat_range_rec; lia. + 2: rewrite length_map; rewrite length_nat_range_rec; lia. symmetry. rewrite map_fold_left_subst_var_in_Z_tup_reindexer; eauto with reindexers. @@ -1042,10 +1042,10 @@ Proof. simpl. repeat rewrite map_fold_left_subst_var_in_Z_tup_combine; eauto with reindexers. - 2: rewrite map_length; rewrite length_nat_range_rec; lia. + 2: rewrite length_map; rewrite length_nat_range_rec; lia. rewrite fold_left_subst_var_in_Z_tup_ZLit. rewrite map_fold_left_subst_var_in_Z_tup_shape_to_index. - 2: unfold shape_to_vars; unfold nat_range; rewrite map_length; + 2: unfold shape_to_vars; unfold nat_range; rewrite length_map; rewrite length_nat_range_rec; lia. rewrite fold_left_subst_var_in_Z_tup_id. 2: { simpl. invert Hlo. rewrite H0. sets. } @@ -1665,14 +1665,14 @@ Proof. erewrite index_to_partial_function_subst_vars. 2: { eapply forall_shape_to_vars_not_in_dom; eauto. } - 2: { rewrite map_length. unfold nat_range. rewrite length_nat_range_rec. - rewrite map_length. eapply length_mesh_grid_indices. + 2: { rewrite length_map. unfold nat_range. rewrite length_nat_range_rec. + rewrite length_map. eapply length_mesh_grid_indices. repeat decomp_goal_index. eauto. } symmetry. erewrite index_to_partial_function_subst_vars. 2: { eapply forall_map_not_in_dom; eauto. } - 2: { rewrite map_length. unfold nat_range. rewrite length_nat_range_rec. - rewrite map_length. eapply length_mesh_grid_indices. + 2: { rewrite length_map. unfold nat_range. rewrite length_nat_range_rec. + rewrite length_map. eapply length_mesh_grid_indices. repeat decomp_goal_index. eauto. } rewrite map_fold_left_subst_var_in_Z_tup_reindexer; eauto with reindexers. symmetry. @@ -1682,13 +1682,13 @@ Proof. simpl. repeat rewrite fold_left_subst_var_in_Z_tup_ZLit. rewrite map_fold_left_subst_var_in_Z_tup_combine. - 2: { rewrite map_length. rewrite length_nat_range_rec. rewrite map_length. + 2: { rewrite length_map. rewrite length_nat_range_rec. rewrite length_map. eapply length_mesh_grid_indices. decomp_goal_index. auto. } symmetry. rewrite map_fold_left_subst_var_in_Z_tup_combine. - 2: { rewrite map_length. unfold nat_range. - rewrite length_nat_range_rec. rewrite map_length. + 2: { rewrite length_map. unfold nat_range. + rewrite length_nat_range_rec. rewrite length_map. eapply length_mesh_grid_indices. decomp_goal_index. auto. } symmetry. @@ -1785,13 +1785,13 @@ Proof. symmetry in H2. repeat rewrite map_partially_eval_Z_tup_ZLit in H2. eapply injective_index_to_partial_function_ZLit in H2; propositional. - rewrite map_length. rewrite length_nat_range_rec. + rewrite length_map. rewrite length_nat_range_rec. eapply length_mesh_grid_indices_Z. eauto. - rewrite map_length. rewrite length_nat_range_rec. + rewrite length_map. rewrite length_nat_range_rec. eapply length_mesh_grid_indices_Z. eauto. - rewrite map_length. rewrite length_nat_range_rec. + rewrite length_map. rewrite length_nat_range_rec. eapply length_mesh_grid_indices_Z. eauto. - rewrite map_length. rewrite length_nat_range_rec. + rewrite length_map. rewrite length_nat_range_rec. eapply length_mesh_grid_indices_Z. eauto. Qed. @@ -2526,12 +2526,12 @@ Proof. repeat rewrite map_subst_var_in_Z_tup_combine_not_in; eauto with reindexers. unfold subst_var_in_Z_tup. simpl. rewrite index_to_partial_function_subst_vars; eauto with reindexers. - 2: { rewrite map_length. rewrite length_nat_range_rec. rewrite map_length. + 2: { rewrite length_map. rewrite length_nat_range_rec. rewrite length_map. eapply length_mesh_grid_indices. repeat decomp_goal_index. auto. } symmetry. rewrite index_to_partial_function_subst_vars; eauto with reindexers. - 2: { rewrite map_length. rewrite length_nat_range_rec. rewrite map_length. + 2: { rewrite length_map. rewrite length_nat_range_rec. rewrite length_map. eapply length_mesh_grid_indices. repeat decomp_goal_index. auto. } symmetry. @@ -2541,11 +2541,11 @@ Proof. symmetry. simpl. rewrite map_fold_left_subst_var_in_Z_tup_combine; eauto with reindexers. - 2: { rewrite map_length. rewrite length_nat_range_rec. rewrite map_length. + 2: { rewrite length_map. rewrite length_nat_range_rec. rewrite length_map. eapply length_mesh_grid_indices. repeat decomp_goal_index. auto. } rewrite map_fold_left_subst_var_in_Z_tup_combine; eauto with reindexers. - 2: { rewrite map_length. rewrite length_nat_range_rec. rewrite map_length. + 2: { rewrite length_map. rewrite length_nat_range_rec. rewrite length_map. eapply length_mesh_grid_indices. repeat decomp_goal_index. auto. } rewrite fold_left_subst_var_in_Z_tup_id. diff --git a/src/verified_lowering/proof/InterpretReindexer.v b/src/verified_lowering/proof/InterpretReindexer.v index 833e27c..5b051dc 100644 --- a/src/verified_lowering/proof/InterpretReindexer.v +++ b/src/verified_lowering/proof/InterpretReindexer.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. @@ -32,7 +32,7 @@ Hint Resolve no_dup_var_generation no_dup_mesh_grid not_var_generation_in_dom2 not_var_generation_in_index2 not_var_generation_in_index not_var_generation_in_dom : reindexers. Hint Extern 3 (Datatypes.length _ = Datatypes.length _) => - rewrite map_length; rewrite length_nat_range_rec; + rewrite length_map; rewrite length_nat_range_rec; eapply length_mesh_grid_indices; eassumption : reindexers. Lemma flatten_index_to_function_alt : forall sh args, @@ -50,21 +50,21 @@ Proof. simpl. erewrite eval_Zexpr_Z_flatten_index_flatten. 2: { econstructor. eauto. rewrite map_snd_combine - by (repeat rewrite map_length; simpl; try lia). + by (repeat rewrite length_map; simpl; try lia). eapply eval_Zexprlist_map_ZLit. } 2: { econstructor. eauto. rewrite map_fst_combine - by (repeat rewrite map_length; simpl; try lia). + by (repeat rewrite length_map; simpl; try lia). eapply eval_Zexprlist_map_ZLit. } rewrite map_snd_combine - by (repeat rewrite map_length; simpl; try lia). + by (repeat rewrite length_map; simpl; try lia). erewrite eval_Zexpr_Z_fold_left_ZTimes. 2: eapply eval_Zexprlist_map_ZLit. 2: eauto. unfold flatten_index. simpl. rewrite map_snd_combine - by (repeat rewrite map_length; simpl; try lia). + by (repeat rewrite length_map; simpl; try lia). rewrite map_fst_combine - by (repeat rewrite map_length; simpl; try lia). + by (repeat rewrite length_map; simpl; try lia). erewrite eval_Zexpr_Z_flatten_index_flatten. 2: { econstructor. eauto. eapply eval_Zexprlist_map_ZLit. } 2: { econstructor. eauto. eapply eval_Zexprlist_map_ZLit. } @@ -111,7 +111,7 @@ Proof. rewrite flatten_index_to_function_alt. reflexivity. eapply length_mesh_grid_indices_Z. auto. - rewrite map_length. rewrite length_nat_range_rec. + rewrite length_map. rewrite length_nat_range_rec. eapply length_mesh_grid_indices_Z in H. simpl in *. lia. eapply no_dup_var_generation. eauto with reindexers. @@ -346,11 +346,11 @@ Proof. reflexivity. erewrite <- in_mesh_grid_cons__. propositional. - rewrite map_length. rewrite length_nat_range_rec. + rewrite length_map. rewrite length_nat_range_rec. eapply length_mesh_grid_indices_Z. auto. eapply no_dup_var_generation. eauto with reindexers. - rewrite map_length. rewrite length_nat_range_rec. + rewrite length_map. rewrite length_nat_range_rec. eapply length_mesh_grid_indices_Z. auto. Qed. @@ -416,7 +416,7 @@ Lemma partial_interpret_reindexer_vars_None : Proof. unfold partial_interpret_reindexer. unfold index_to_partial_function. intros. unfold shape_to_vars. - rewrite map_length. unfold nat_range. rewrite length_nat_range_rec. + rewrite length_map. unfold nat_range. rewrite length_nat_range_rec. eapply Nat.eqb_neq in H. rewrite H. auto. Qed. @@ -430,7 +430,7 @@ Proof. cases (Datatypes.length (shape_to_vars sh) =? Datatypes.length args)%nat. - eapply Nat.eqb_eq in Heq. unfold shape_to_vars in *. - rewrite map_length in *. unfold nat_range in *. + rewrite length_map in *. unfold nat_range in *. rewrite length_nat_range_rec in *. auto. - discriminate. Qed. diff --git a/src/verified_lowering/proof/ListMisc.v b/src/verified_lowering/proof/ListMisc.v index 6e5f0b7..fb9d504 100644 --- a/src/verified_lowering/proof/ListMisc.v +++ b/src/verified_lowering/proof/ListMisc.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Import ListNotations. Open Scope list_scope. @@ -189,7 +189,7 @@ Lemma length_concat {X} : forall (l : list (list X)) k, Proof. induct l; intros. - reflexivity. - - simpl. rewrite app_length. invert H. + - simpl. rewrite length_app. invert H. f_equal. eapply IHl. auto. Qed. @@ -904,20 +904,20 @@ Proof. cases (rev (truncl_list k (rev l ++ [a]))). * erewrite rev_arg_empty in Heq. eapply truncl_list_length_empty in Heq. - rewrite app_length in *. rewrite rev_length in *. simpl in Heq. + rewrite length_app in *. rewrite length_rev in *. simpl in Heq. simpl length in H. lia. * simpl length in H. assert (k = length l \/ k <> length l) by lia. invert H0. -- rewrite truncl_list_app in Heq. - 2: try rewrite rev_length; lia. + 2: try rewrite length_rev; lia. rewrite rev_app_distr in Heq. simpl in Heq. invert Heq. auto. -- rewrite truncl_list_app in Heq. rewrite rev_app_distr in Heq. simpl in Heq. invert Heq. auto. - rewrite rev_length. lia. + rewrite length_rev. lia. + simpl. simpl length in H. - rewrite truncl_list_app by (rewrite rev_length; lia). + rewrite truncl_list_app by (rewrite length_rev; lia). rewrite rev_app_distr. simpl. eapply IHl. lia. Qed. @@ -999,11 +999,11 @@ Proof. assert (k < length l \/ k >= length l) as Hcase by lia. inversion Hcase as [ Hcase1 | Hcase2 ]; clear Hcase. + replace (k - length (rev l)) with 0. - 2: { rewrite rev_length. lia. } + 2: { rewrite length_rev. lia. } simpl. rewrite rev_app_distr. simpl. econstructor. eauto. eauto. + rewrite skipn_all2. - 2: { rewrite rev_length. lia. } - simpl. rewrite rev_length. + 2: { rewrite length_rev. lia. } + simpl. rewrite length_rev. cases (k - length l). simpl. econstructor. auto. rewrite firstn_nil. auto. simpl. rewrite skipn_nil. simpl. eauto. @@ -1049,7 +1049,7 @@ Proof. induct l; intros. - rewrite @nth_error_empty in *. discriminate. - simpl. - rewrite firstn_app. rewrite rev_length. simpl length in *. + rewrite firstn_app. rewrite length_rev. simpl length in *. eapply in_or_app. cases x. + simpl in H. invert H. @@ -1128,7 +1128,7 @@ Proof. cases (length (x::l) - n). + simpl. rewrite skipn_all2 with (n:=n). - 2: { rewrite rev_length. simpl length in *. lia. } + 2: { rewrite length_rev. simpl length in *. lia. } rewrite skipn_nil. auto. + rewrite firstn_cons. rewrite skipn_cons. simpl length in Heq. @@ -1136,7 +1136,7 @@ Proof. replace l with (rev (rev l)) at 1. 2: rewrite rev_involutive; auto. rewrite firstn_rev. - rewrite rev_length. + rewrite length_rev. f_equal. f_equal. f_equal. lia. Qed. @@ -1189,13 +1189,13 @@ Proof. rewrite sub_0_r. cases (length l - n). + simpl. rewrite nth_error_app2. - 2: { rewrite rev_length. lia. } - rewrite rev_length. + 2: { rewrite length_rev. lia. } + rewrite length_rev. assert (n = length l) by lia. subst. rewrite sub_diag. reflexivity. + simpl. rewrite nth_error_app1. - 2: { rewrite rev_length. lia. } + 2: { rewrite length_rev. lia. } erewrite <- IHl. 2: reflexivity. 2: lia. f_equal. lia. @@ -1291,7 +1291,7 @@ Proof. assert (k < length l \/ length l <= k) by lia. invert H0. - rewrite nth_error_app1. auto. - rewrite firstn_length. rewrite min_l by lia. lia. + rewrite length_firstn. rewrite min_l by lia. lia. - rewrite firstn_all2 by auto. rewrite skipn_all2 by lia. rewrite app_nil_r. eauto. Qed. @@ -1303,11 +1303,11 @@ Lemma nth_error_skipn_mod {X} : forall x (l : list X) k, Proof. intros. symmetry. rewrite <- (firstn_skipn (k * (x / k)) l) at 1. rewrite nth_error_app2. - 2: { rewrite firstn_length. rewrite min_l. + 2: { rewrite length_firstn. rewrite min_l. eapply Div0.mul_div_le. eapply le_trans. eapply Div0.mul_div_le. lia. } - rewrite firstn_length. + rewrite length_firstn. rewrite min_l. 2: { eapply le_trans. eapply Div0.mul_div_le. lia. } rewrite Div0.mod_eq by lia. eauto. diff --git a/src/verified_lowering/proof/LowerCorrect.v b/src/verified_lowering/proof/LowerCorrect.v index 092d817..6bdafe5 100644 --- a/src/verified_lowering/proof/LowerCorrect.v +++ b/src/verified_lowering/proof/LowerCorrect.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. @@ -32,7 +32,7 @@ Hint Resolve no_dup_var_generation no_dup_mesh_grid not_var_generation_in_dom2 not_var_generation_in_index2 not_var_generation_in_index not_var_generation_in_dom : reindexers. Hint Extern 3 (Datatypes.length _ = Datatypes.length _) => - rewrite map_length; rewrite length_nat_range_rec; + rewrite length_map; rewrite length_nat_range_rec; eapply length_mesh_grid_indices; eassumption : reindexers. Arguments flatten : simpl nomatch. @@ -2771,7 +2771,7 @@ eapply H6 with (st:=st) (st':=st') (asn:=asm). assert (-1 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)) < z0 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)))%Z by lia. - eapply Zmult_lt_reg_r in H17. + apply Zorder.Zmult_lt_reg_r in H17. lia. lia. rewrite Nat2Z.inj_mul in H16. rewrite @@ -2781,7 +2781,7 @@ eapply H6 with (st:=st) (st':=st') (asn:=asm). assert (-1 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)) < z0 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)))%Z by lia. - eapply Zmult_lt_reg_r in H17. + eapply Zorder.Zmult_lt_reg_r in H17. lia. lia. lia. repeat decomp_goal_index. propositional. @@ -2791,7 +2791,7 @@ eapply H6 with (st:=st) (st':=st') (asn:=asm). assert (-1 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)) < z0 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)))%Z by lia. - eapply Zmult_lt_reg_r in H17. + eapply Zorder.Zmult_lt_reg_r in H17. lia. lia. rewrite Nat2Z.inj_mul in H16. rewrite @@ -2801,7 +2801,7 @@ eapply H6 with (st:=st) (st':=st') (asn:=asm). assert (-1 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)) < z0 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)))%Z by lia. - eapply Zmult_lt_reg_r in H17. + eapply Zorder.Zmult_lt_reg_r in H17. lia. lia. eauto. eauto. lia. lia. @@ -2871,7 +2871,7 @@ eapply H6 with (st:=st) (st':=st') (asn:=asm). { pose proof (truncl_list_length_empty (Z.to_nat (eval_Zexpr_Z_total $0 k)) (rev l)). - erewrite rev_length in H6. + erewrite length_rev in H6. erewrite result_has_shape_length in H6. 2: { simpl map in *. eauto. } assert (Z.to_nat (eval_Zexpr_Z_total $0 m) <= @@ -2889,7 +2889,7 @@ eapply H6 with (st:=st) (st':=st') (asn:=asm). 2: { eauto. } simpl in H12. invs. rewrite firstn_all2 in H12. - 2: { erewrite rev_length. erewrite result_has_shape_length. + 2: { erewrite length_rev. erewrite result_has_shape_length. 2: simpl in *; eauto. lia. } clear H9. clear H14. clear H6. eapply Forall_rev in H12. rewrite rev_involutive in *. @@ -3108,7 +3108,7 @@ eapply H6 with (st:=st) (st':=st') (asn:=asm). cases (reindexer (let (v0, d) := p0 in (v0, (d - k)%z) :: l2)). { unfold result_shape_Z, shape_to_index, shape_to_vars in Heq. simpl in *. invert Heq. - rewrite map_length in *. + rewrite length_map in *. cases l. - simpl in *. invert H13. eapply reindexer_not_empty_vars_in_index in Heq0. @@ -3140,7 +3140,7 @@ eapply H6 with (st:=st) (st':=st') (asn:=asm). cases (reindexer (let (v, d) := p0 in (v, (d - k)%z) :: l2)). { unfold result_shape_Z, shape_to_index, shape_to_vars in Heq. simpl in *. invert Heq. - rewrite map_length in *. + rewrite length_map in *. cases l. - simpl in *. invert H8. eapply reindexer_not_empty_vars_in_index in Heq0. @@ -3183,7 +3183,7 @@ eapply H6 with (st:=st) (st':=st') (asn:=asm). simpl in *. eauto. } unfold result_shape_Z, shape_to_index, shape_to_vars in Heq1. simpl in *. - rewrite map_length in *. + rewrite length_map in *. cases (Z.to_nat (eval_Zexpr_Z_total $0 m) - Z.to_nat (eval_Zexpr_Z_total $0 k)). - simpl in *. @@ -3254,8 +3254,8 @@ eapply H6 with (st:=st) (st':=st') (asn:=asm). eapply forall_eq_gen_pad in H11. simpl in H11. rewrite H11. - rewrite rev_repeat. rewrite firstn_length. - rewrite rev_length. + rewrite rev_repeat. rewrite length_firstn. + rewrite length_rev. erewrite result_has_shape_length by eauto. f_equal. lia. } invs. @@ -3708,7 +3708,7 @@ eapply H6 with (st:=st) (st':=st') (asn:=asm). ((v0 - k)%z, (d - k)%z) :: l2)). { unfold shape_to_index,result_shape_Z,shape_to_vars in Heq. simpl in Heq. invert Heq. - repeat rewrite map_length in *. + repeat rewrite length_map in *. cases l. - simpl in *. invert H12. eapply reindexer_not_empty_vars_in_index in Heq0. @@ -3747,7 +3747,7 @@ eapply H6 with (st:=st) (st':=st') (asn:=asm). cases (reindexer (let (v, d) := p0 in ((v - k)%z, (d - k)%z) :: l2)). { unfold shape_to_index,result_shape_Z,shape_to_vars in Heq. simpl in Heq0. invert Heq. - repeat rewrite map_length in *. + repeat rewrite length_map in *. cases l. - simpl in *. invert H9. eapply reindexer_not_empty_vars_in_index in Heq0. @@ -3847,7 +3847,7 @@ eapply H6 with (st:=st) (st':=st') (asn:=asm). eapply forall_eq_gen_pad in H6. simpl in H6. rewrite H6. - rewrite firstn_length. + rewrite length_firstn. erewrite result_has_shape_length by eauto. f_equal. lia. } invs. diff --git a/src/verified_lowering/proof/LowerExists.v b/src/verified_lowering/proof/LowerExists.v index 1ad6387..8a0cc3d 100644 --- a/src/verified_lowering/proof/LowerExists.v +++ b/src/verified_lowering/proof/LowerExists.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. @@ -31,7 +31,7 @@ Hint Resolve no_dup_var_generation no_dup_mesh_grid not_var_generation_in_dom2 not_var_generation_in_index2 not_var_generation_in_index not_var_generation_in_dom : reindexers. Hint Extern 3 (Datatypes.length _ = Datatypes.length _) => - rewrite map_length; rewrite length_nat_range_rec; + rewrite length_map; rewrite length_nat_range_rec; eapply length_mesh_grid_indices; eassumption : reindexers. Arguments flatten : simpl nomatch. @@ -2159,7 +2159,7 @@ sets. eapply forall_eq_gen_pad in H8. rewrite H8. simpl gen_pad_list. rewrite rev_repeat. - rewrite firstn_length. rewrite rev_length. + rewrite length_firstn. rewrite length_rev. erewrite result_has_shape_length. 2: { eapply constant_nonneg_bounds_size_of_eval_expr_result_has_shape in H2; eauto. } @@ -2206,10 +2206,10 @@ sets. eapply well_formed_reindexer_truncr. rewrite rev_app_distr. rewrite truncl_list_app. - 2: { rewrite rev_length. simpl. rewrite repeat_length. lia. } + 2: { rewrite length_rev. simpl. rewrite repeat_length. lia. } rewrite truncl_list_skipn. rewrite skipn_all2. - 2: { rewrite rev_length. simpl. rewrite repeat_length. lia. } + 2: { rewrite length_rev. simpl. rewrite repeat_length. lia. } replace (Z.to_nat (eval_Zexpr_Z_total $0 m)) with (length l). 2: { erewrite result_has_shape_length by eauto. reflexivity. } rewrite <- skipn_rev. simpl. @@ -2218,7 +2218,7 @@ sets. eapply Forall_app. split. eapply forall_firstn. eapply result_has_shape_forall. eauto. simpl. eapply Forall_repeat. eapply result_has_shape_gen_pad. - rewrite app_length. simpl. rewrite firstn_length. + rewrite length_app. simpl. rewrite length_firstn. rewrite repeat_length. erewrite result_has_shape_length by eauto. rewrite min_l by lia. rewrite sub_add. reflexivity. lia. apply Henv. eauto. lia. lia. @@ -2234,7 +2234,7 @@ sets. eapply forall_eq_gen_pad in H8. rewrite H8. simpl gen_pad_list. rewrite rev_repeat. - rewrite firstn_length. rewrite rev_length. + rewrite length_firstn. rewrite length_rev. erewrite result_has_shape_length. 2: { eapply constant_nonneg_bounds_size_of_eval_expr_result_has_shape in H2; eauto. } @@ -2243,10 +2243,10 @@ sets. eapply well_formed_allocation_truncr. rewrite rev_app_distr. rewrite truncl_list_app. - 2: { rewrite rev_length. simpl. rewrite repeat_length. lia. } + 2: { rewrite length_rev. simpl. rewrite repeat_length. lia. } rewrite truncl_list_skipn. rewrite skipn_all2. - 2: { rewrite rev_length. simpl. rewrite repeat_length. lia. } + 2: { rewrite length_rev. simpl. rewrite repeat_length. lia. } replace (Z.to_nat (eval_Zexpr_Z_total $0 m)) with (length l). 2: { erewrite result_has_shape_length by eauto. reflexivity. } simpl. @@ -2256,7 +2256,7 @@ sets. eapply Forall_app. split. eapply forall_firstn. eapply result_has_shape_forall. eauto. simpl. eapply Forall_repeat. eapply result_has_shape_gen_pad. - rewrite app_length. simpl. rewrite firstn_length. + rewrite length_app. simpl. rewrite length_firstn. rewrite repeat_length. erewrite result_has_shape_length by eauto. rewrite min_l by lia. rewrite sub_add. reflexivity. lia. lia. apply Hrdx. eauto. apply Henv. apply Hrdx. apply Hrdx. @@ -2288,7 +2288,7 @@ sets. eapply forall_eq_gen_pad in H10. rewrite H10. simpl gen_pad_list. - rewrite firstn_length. + rewrite length_firstn. erewrite result_has_shape_length. 2: { eauto. } @@ -2340,9 +2340,9 @@ sets. eapply Forall_app. split. simpl. eapply Forall_repeat. eapply result_has_shape_gen_pad. eapply forall_skipn. eapply result_has_shape_forall. eauto. - rewrite app_length. simpl. rewrite skipn_length. + rewrite length_app. simpl. rewrite length_skipn. rewrite repeat_length. erewrite result_has_shape_length by eauto. - rewrite le_plus_minus_r. reflexivity. lia. + instantiate (1 := m). lia. apply Henv. eauto. lia. lia. eauto. lia. apply Hrdx. @@ -2353,7 +2353,7 @@ sets. eapply forall_eq_gen_pad in H10. rewrite H10. simpl gen_pad_list. - rewrite firstn_length. + rewrite length_firstn. erewrite result_has_shape_length by eauto. rewrite min_l by lia. @@ -2363,9 +2363,9 @@ sets. eapply Forall_app. split. simpl. eapply Forall_repeat. eapply result_has_shape_gen_pad. eapply forall_skipn. eapply result_has_shape_forall. eauto. - rewrite app_length. simpl. rewrite skipn_length. + rewrite length_app. simpl. rewrite length_skipn. rewrite repeat_length. erewrite result_has_shape_length by eauto. - rewrite le_plus_minus_r. reflexivity. lia. lia. + instantiate (1 := m). lia. lia. apply Hrdx. eauto. eauto. apply Henv. apply Hrdx. apply Hrdx. - invert Hsize. eq_size_of. invert H4. invert Hconst. invs. pose proof H4. diff --git a/src/verified_lowering/proof/Meshgrid.v b/src/verified_lowering/proof/Meshgrid.v index c24ea70..24859c3 100644 --- a/src/verified_lowering/proof/Meshgrid.v +++ b/src/verified_lowering/proof/Meshgrid.v @@ -7,7 +7,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. @@ -78,7 +78,7 @@ Proof. rewrite succ_repeat_app_end. rewrite concat_app. rewrite map2_app. - 2:{ erewrite length_concat. rewrite map_length. + 2:{ erewrite length_concat. rewrite length_map. rewrite length_zrange'. all: cycle 1. eapply Forall_map. @@ -102,7 +102,7 @@ Proof. rewrite succ_repeat_app_end in H. rewrite concat_app in H. rewrite map2_app in H. - 2:{ erewrite length_concat. rewrite map_length. + 2:{ erewrite length_concat. rewrite length_map. rewrite length_zrange'. all: cycle 1. eapply Forall_map. @@ -150,7 +150,7 @@ Proof. rewrite Z.sub_0_r in IHk. setoid_rewrite Nat2Z.id in IHk. rewrite map2_app. 2: { erewrite length_concat. - rewrite map_length. rewrite length_zrange'. + rewrite length_map. rewrite length_zrange'. erewrite length_concat. rewrite repeat_length. reflexivity. eapply Forall_repeat. reflexivity. @@ -299,7 +299,7 @@ Proof. erewrite length_concat. 2: { eapply Forall_map. eapply Forall_forall. intros. rewrite repeat_length. reflexivity. } - rewrite map_length. unfold zrange. + rewrite length_map. unfold zrange. rewrite length_zrange'. rewrite Z.sub_0_r. erewrite length_concat. @@ -395,7 +395,7 @@ Proof. erewrite length_concat. 2: { eapply Forall_map. simpl. eapply Forall_forall. intros. reflexivity. } - rewrite map_length. unfold zrange. + rewrite length_map. unfold zrange. rewrite length_zrange'. lia. + cases x. eapply not_In_empty_map2_cons in H5. propositional. replace (z * fold_left Z.mul (z0 :: sh) 1)%Z with @@ -569,7 +569,7 @@ Proof. by lia. invert H3. * rewrite H4. lia. - * eapply Zle_mult_approx. lia. lia. lia. + * eapply auxiliary.Zle_mult_approx. lia. lia. lia. Qed. Lemma exists_0_empty_mesh_grid : forall l, @@ -640,7 +640,7 @@ Proof. erewrite length_concat. 2: { eapply Forall_forall. intros. eapply repeat_spec in H1. subst. reflexivity. } - rewrite map_length. rewrite length_zrange'. + rewrite length_map. rewrite length_zrange'. rewrite repeat_length. lia. rewrite map_id. reflexivity. Qed. @@ -981,7 +981,7 @@ Proof. repeat rewrite map_cons. pose proof (result_has_shape_length _ _ _ H). - rewrite app_length in H1. + rewrite length_app in H1. rewrite repeat_length in H1. cases (Z.to_nat (eval_Zexpr_Z_total $0 m)). @@ -1082,7 +1082,7 @@ Proof. repeat rewrite map_cons. pose proof (result_has_shape_length _ _ _ H). - rewrite app_length in H1. + rewrite length_app in H1. rewrite repeat_length in H1. cases (Z.to_nat (eval_Zexpr_Z_total $0 m)). diff --git a/src/verified_lowering/proof/Pad.v b/src/verified_lowering/proof/Pad.v index 6167fce..0d6900e 100644 --- a/src/verified_lowering/proof/Pad.v +++ b/src/verified_lowering/proof/Pad.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. @@ -323,7 +323,7 @@ Proof. rewrite H2,H4 in *. eapply add_list_repeat_gen_pad in a. 2: { reflexivity. } - 2: { simpl. repeat rewrite firstn_length. + 2: { simpl. repeat rewrite length_firstn. eapply add_list_length in H7. rewrite H7. reflexivity. } rewrite a. eapply Forall_repeat. eauto. @@ -334,7 +334,7 @@ Proof. rewrite H0, H1 in *. eapply add_list_repeat_gen_pad in a. 2: { reflexivity. } - 2: { repeat rewrite firstn_length. repeat rewrite rev_length. + 2: { repeat rewrite length_firstn. repeat rewrite length_rev. eapply add_list_length in H7. rewrite H7. reflexivity. } rewrite a. eapply Forall_repeat. eauto. @@ -347,7 +347,7 @@ Proof. eapply Forall_rev. eapply Forall_rev in H5,H8. rewrite rev_involutive in *. rewrite skipn_firstn_comm in H5,H8. rewrite skipn_firstn_comm. - repeat rewrite firstn_length in *. rewrite min_l in * by lia. + repeat rewrite length_firstn in *. rewrite min_l in * by lia. pose proof a. pose proof a. eapply add_list_result_length in H9. eapply add_list_length in H7. @@ -498,14 +498,14 @@ Proof. { (* H0 *) cases r1. lia. simpl rev in H0. rewrite firstn_app in H0. - rewrite rev_length in *. + rewrite length_rev in *. eapply Forall_app in H0. invs. rewrite firstn_all2 in H6. 2: { simpl length. lia. } invert H6. rewrite H10. eapply result_lookup_Z_gen_pad. eauto. } invert H. { invs. simpl in *. rewrite skipn_app in *. rewrite firstn_app in *. - rewrite skipn_length in *. rewrite rev_length in *. + rewrite length_skipn in *. rewrite length_rev in *. eapply Forall_app in H0. eapply Forall_app in H9. invs. cases l. 2: lia. simpl in *. clear H3. clear H4. clear H2. @@ -525,7 +525,7 @@ Proof. intros. inversion 1. } invs. simpl in *. rewrite skipn_app in *. rewrite firstn_app in *. - rewrite skipn_length in *. rewrite rev_length in *. + rewrite length_skipn in *. rewrite length_rev in *. eapply Forall_app in H0. eapply Forall_app in H9. invs. replace (r1 - length r0) with 0 in * by lia. simpl in H10. rewrite firstn_all2 in H10 by (simpl; lia). @@ -547,7 +547,7 @@ Proof. cases l. lia. simpl in H4. invert H4. { rewrite <- firstn_skipn with (n:=l) (l:=r0) in Heq0. rewrite nth_error_app1 in Heq0. - 2: { rewrite firstn_length. lia. } + 2: { rewrite length_firstn. lia. } eapply nth_error_In in Heq0. eapply Forall_forall in H12. 2: eassumption. subst. @@ -568,11 +568,11 @@ Proof. pose proof Heq0 as HH. rewrite <- firstn_skipn with (n:=l) (l:=r::r0) in HH. rewrite nth_error_app2 in HH. - 2: { rewrite firstn_length. lia. } - rewrite firstn_length in *. + 2: { rewrite length_firstn. lia. } + rewrite length_firstn in *. rewrite <- firstn_skipn with (n:= l') (l:=(skipn l (r::r0))) in HH. rewrite nth_error_app1 in HH. - 2: { rewrite firstn_length. rewrite skipn_length. + 2: { rewrite length_firstn. rewrite length_skipn. simpl length in *. lia. } eapply nth_error_In in HH. eapply Forall_forall in H7. 2: eassumption. @@ -629,14 +629,14 @@ Proof. pose proof Heq0 as HH. rewrite <- @rev_involutive with (l:=r0) in HH. erewrite <- nth_error_rev in HH. - 2: { rewrite rev_length. reflexivity. } + 2: { rewrite length_rev. reflexivity. } rewrite <- firstn_skipn with (n:=r1) (l:=rev r0) in HH. rewrite nth_error_app2 in HH. - 2: { rewrite firstn_length. rewrite rev_length. lia. } - rewrite firstn_length in *. rewrite rev_length in *. + 2: { rewrite length_firstn. rewrite length_rev. lia. } + rewrite length_firstn in *. rewrite length_rev in *. rewrite <- firstn_skipn with (n:= r') (l:=(skipn r1 (rev r0))) in HH. rewrite nth_error_app1 in HH. - 2: { rewrite firstn_length. rewrite skipn_length. rewrite rev_length. + 2: { rewrite length_firstn. rewrite length_skipn. rewrite length_rev. simpl length in *. lia. } eapply nth_error_In in HH. eapply Forall_forall in H. 2: eassumption. @@ -765,7 +765,10 @@ Proof. reflexivity. - invert H1. Qed. -*) + *) +Lemma minus_plus a b : a + b - a = b. +Proof. lia. Qed. + Lemma has_pad_size_of_relate_pads_gen_pad : forall e v size sh g pads, size_of e size -> @@ -962,7 +965,7 @@ Proof. rewrite firstn_all2 in H17. 2: { rewrite repeat_length. lia. } invert H17. eapply Forall_repeat. eauto. - + eapply beq_nat_false in Heq1. + + apply Nat.eqb_neq in Heq1. replace (Datatypes.S n1 + n * Datatypes.S n1) with (Datatypes.S n * Datatypes.S n1) by lia. rewrite <- mul_sub_distr_r. @@ -1477,14 +1480,14 @@ Proof. split. rewrite <- (firstn_skipn (x * Z.to_nat (eval_Zexpr_Z_total $0 m0)) (flatten_result l)). - rewrite firstn_app. rewrite firstn_length. + rewrite firstn_app. rewrite length_firstn. erewrite result_has_shape_length. 2: { eauto. } rewrite mul_min_distr_r. replace (min x (Z.to_nat (eval_Zexpr_Z_total $0 n0))) with x by lia. rewrite minus_plus. rewrite firstn_all2. - 2: { rewrite firstn_length. erewrite result_has_shape_length by eauto. + 2: { rewrite length_firstn. erewrite result_has_shape_length by eauto. rewrite mul_min_distr_r. rewrite min_l by lia. eapply le_add_r. } @@ -1504,25 +1507,23 @@ Proof. simpl. intros. cases a0. propositional. invs. eauto. eapply forall_result_has_shape. eapply forall_skipn. - eapply result_has_shape_forall. eauto. rewrite skipn_length. auto. + eapply result_has_shape_forall. eauto. rewrite length_skipn. auto. lia. } split. rewrite <- (firstn_skipn (y * Z.to_nat (eval_Zexpr_Z_total $0 m0)) (rev (flatten_result l))). - rewrite firstn_app. rewrite firstn_length. rewrite rev_length. + rewrite firstn_app. rewrite length_firstn. rewrite length_rev. erewrite result_has_shape_length. 2: { eauto. } rewrite mul_min_distr_r. replace (min y (Z.to_nat (eval_Zexpr_Z_total $0 n0))) with y by lia. rewrite minus_plus. rewrite firstn_all2. - 2: { rewrite firstn_length. - rewrite rev_length. + 2: { rewrite length_firstn. + rewrite length_rev. erewrite result_has_shape_length by eauto. - rewrite mul_min_distr_r. - rewrite min_l by lia. - eapply le_plus_l. } + set (x1 := _ * _). set (x2 := _ * _). set (x3 := _ * _). lia. } eapply Forall_app. split. eapply forall_firstn_rev_flatten_result. eauto. eauto. @@ -1596,7 +1597,7 @@ Proof. erewrite <- result_has_shape_filter_until_0. eauto. rewrite <- H10. eapply relate_pads_filter_until_0; eauto. - + eapply beq_nat_false in Heq. + + apply Nat.eqb_neq in Heq. replace (flatten_result (skipn x l)) with (skipn 0 (flatten_result (skipn x l))) by eauto. eapply forall_firstn_skipn_flatten_result. @@ -1692,7 +1693,7 @@ Proof. 2: { eapply result_has_shape_flatten. eapply result_has_shape_rev. eapply forall_result_has_shape. eapply forall_skipn. eapply Forall_rev. eapply result_has_shape_forall. eauto. - rewrite skipn_length. rewrite rev_length. + rewrite length_skipn. rewrite length_rev. erewrite result_has_shape_length by eauto. reflexivity. } rewrite <- mul_sub_distr_r. @@ -1703,16 +1704,16 @@ Proof. reflexivity. } eapply Forall_rev. rewrite skipn_rev. - rewrite skipn_length. rewrite rev_length. + rewrite length_skipn. rewrite length_rev. erewrite result_has_shape_length by eauto. cases (Z.to_nat (eval_Zexpr_Z_total $0 n0) - y - Datatypes.S r). simpl. * rewrite sub_0_r. rewrite firstn_all2 in H13. - 2: { rewrite skipn_length. rewrite rev_length. + 2: { rewrite length_skipn. rewrite length_rev. erewrite result_has_shape_length by eauto. lia. } rewrite firstn_all2. - 2: { rewrite skipn_length. rewrite rev_length. + 2: { rewrite length_skipn. rewrite length_rev. erewrite result_has_shape_length by eauto. lia. } eapply forall_flatten_result_rev. 2: { eapply forall_result_has_shape. eapply forall_skipn. @@ -1725,7 +1726,7 @@ Proof. 2: { eapply forall_skipn. eapply Forall_rev. eapply Hconst'. } simpl in *. rewrite firstn_all2 in H16. - 2: { rewrite rev_length. + 2: { rewrite length_rev. erewrite result_has_shape_length by eauto. lia. } eapply Forall_rev in H16. rewrite rev_involutive in H16. eapply Forall_forall. intros. eapply Forall_forall in H16. @@ -1754,7 +1755,7 @@ Proof. eapply forall_skipn. eapply Forall_rev. eapply Hconst'. } simpl in *. rewrite firstn_all2 in H16. - 2: { rewrite rev_length. + 2: { rewrite length_rev. erewrite result_has_shape_length by eauto. lia. } eapply Forall_rev in H16. rewrite rev_involutive in H16. eapply Forall_forall. intros. eapply Forall_forall in H16. @@ -1941,7 +1942,7 @@ Proof. (Datatypes.S (Datatypes.length l)) (Z.to_nat (eval_Zexpr_Z_total $0 k))). lia. } - rewrite sub_0_r. rewrite skipn_length. + rewrite sub_0_r. rewrite length_skipn. reflexivity. } rewrite firstn_map. unfold nat_range. rewrite firstn_rev_nat_range_rec. rewrite add_0_l. @@ -1959,11 +1960,9 @@ Proof. assert ((c mod kk + (kk - mm mod kk) mod kk) / kk <= 1). eapply add_mod_div_bound. lia. cases ((c mod kk + (kk - mm mod kk) mod kk) / kk). - rewrite add_0_r. eapply le_trans. - 2: { eapply le_plus_l. } + enough (c / kk <= mm / kk) by lia. eapply div_le_mono. lia. lia. - cases n1. 2: lia. - eapply plus_le_compat_r. + enough (c / kk <= mm / kk) by lia. eapply div_le_mono. lia. lia. cases (mm //n kk - mm / kk). eapply mod_0_iff_ceil_sub_floor_0 in Heq0. lia. lia. @@ -2025,7 +2024,7 @@ Proof. rewrite <- firstn_rev. simpl length. rewrite Hlen. rewrite <- mod_eq. rewrite firstn_all2. - 2: { rewrite rev_length. rewrite firstn_length. + 2: { rewrite length_rev. rewrite length_firstn. pose proof (Nat.mod_upper_bound mm kk). lia. } eapply Forall_rev. eapply forall_firstn_ge. eauto. assert ((c + (kk - mm mod kk) mod kk) < kk \/ @@ -2041,7 +2040,7 @@ Proof. rewrite flatten_result_nat_range_rec. rewrite <- (firstn_skipn (length (r0::l) - c) (r0::l)). rewrite skipn_app. rewrite firstn_app. - rewrite skipn_length. rewrite firstn_length. + rewrite length_skipn. rewrite length_firstn. rewrite <- (rev_involutive (skipn _ (r0::l))). rewrite <- firstn_rev. rewrite Forall_app. split. @@ -2051,7 +2050,7 @@ Proof. eapply Forall_rev. eauto. } simpl length. rewrite Hlen. rewrite skipn_all2. rewrite firstn_nil. econstructor. - rewrite firstn_length. simpl length. rewrite min_l by lia. + rewrite length_firstn. simpl length. rewrite min_l by lia. rewrite mul_sub_distr_r. rewrite mul_add_distr_r. rewrite (Nat.div_mod_eq mm kk) at 1. rewrite mul_comm. @@ -2061,7 +2060,7 @@ Proof. rewrite <- (mod_id mm kk) in H17 at 1. rewrite (Nat.add_comm (mm mod kk)) in H17. rewrite (Nat.add_comm c) in H17. 2: lia. 2: lia. - eapply plus_le_reg_l in H17. + apply add_le_mono_l in H17. rewrite mul_1_l. rewrite mul_comm. rewrite <- Nat.div_mod_eq. rewrite <- (mod_id mm kk) at 3 by lia. @@ -2072,7 +2071,7 @@ Proof. with (mm mod kk + (kk - mm mod kk) mod kk + (c - mm mod kk)) by lia. rewrite mod_id by lia. - eapply plus_le_reg_l with (p:=c). rewrite le_plus_minus_r by lia. + apply add_le_mono_l with (p:=c). rewrite add_sub_assoc by lia. rewrite Nat.add_comm. replace kk with (1*kk) at 4 by lia. rewrite div_add_l by lia. @@ -2114,17 +2113,19 @@ Proof. rewrite (mul_comm _ (Datatypes.S _)). simpl. rewrite sub_add_distr. 2: lia. rewrite mul_comm. rewrite <- Heq0. - rewrite le_plus_minus_r. + rewrite add_sub_assoc. + rewrite minus_plus. 2: { rewrite H17. - eapply plus_le_reg_l with (p:=kk). + eapply add_le_mono_l with (p:=kk). replace (kk + n0 * kk) with (Datatypes.S n0 * kk) by lia. rewrite <- Heq0. - rewrite le_plus_minus_r. + rewrite add_sub_assoc. 2: { rewrite <- H17. assert (kk <= mm \/ mm < kk) by lia. inversion H19. lia. eapply div_small in H20. rewrite H20 in H17. rewrite mul_0_r in *. lia. } rewrite mul_comm. + rewrite minus_plus. eapply mul_le_mono_l. eapply div_le_mono. lia. lia. } @@ -2151,7 +2152,7 @@ Proof. rewrite <- (rev_involutive (skipn _ _)). rewrite <- firstn_rev. rewrite firstn_all2. - 2: { rewrite rev_length. rewrite firstn_length. lia. } + 2: { rewrite length_rev. rewrite length_firstn. lia. } eapply Forall_rev. eapply forall_firstn_ge. eauto. assert (kk <= c \/ c < kk) by lia. cases H19. lia. @@ -2204,7 +2205,7 @@ Proof. { invert H15. } split. rewrite app_comm_cons. rewrite skipn_app. rewrite firstn_app. rewrite firstn_app. rewrite skipn_repeat. rewrite firstn_repeat. - rewrite firstn_repeat. rewrite firstn_length. rewrite skipn_length. + rewrite firstn_repeat. rewrite length_firstn. rewrite length_skipn. rewrite Forall_app. split. { rewrite firstn_firstn. @@ -2327,10 +2328,10 @@ Proof. rewrite rev_app_distr. rewrite firstn_app. rewrite rev_app_distr. rewrite firstn_app. rewrite rev_app_distr. rewrite firstn_app. - repeat rewrite rev_length. repeat rewrite firstn_length. - repeat rewrite skipn_length. repeat rewrite rev_length. - repeat rewrite skipn_length. repeat rewrite firstn_length. - repeat rewrite rev_length. rewrite skipn_length. + repeat rewrite length_rev. repeat rewrite length_firstn. + repeat rewrite length_skipn. repeat rewrite length_rev. + repeat rewrite length_skipn. repeat rewrite length_firstn. + repeat rewrite length_rev. rewrite length_skipn. simpl length. rewrite Hlen. rewrite (sub_sub_distr mm mm c) by lia. rewrite sub_diag. rewrite add_0_l. @@ -2362,8 +2363,7 @@ Proof. assert (mm / kk = Datatypes.S n0 + c /kk). lia. rewrite H19. rewrite mul_add_distr_l. rewrite (Nat.add_comm _ (kk*(c/kk))). - rewrite (mul_comm _ (Datatypes.S _)). simpl. - rewrite add_assoc. eapply le_plus_l. } + rewrite (mul_comm _ (Datatypes.S _)). simpl. lia. } replace (kk * (c / kk) + kk) with (c + ((kk - c mod kk) mod kk)). 2: { rewrite (Nat.div_mod_eq c kk) at 1. rewrite <- add_assoc. rewrite mod_id. auto. lia. unfold not. @@ -2393,11 +2393,11 @@ Proof. rewrite <- (firstn_skipn c (rev (r0::l))). rewrite firstn_app. rewrite rev_app_distr. rewrite firstn_app. rewrite rev_app_distr. rewrite skipn_app. - rewrite firstn_app. repeat rewrite rev_length. rewrite firstn_length. - repeat rewrite firstn_length. repeat rewrite skipn_length. - repeat rewrite rev_length. repeat rewrite firstn_length. - repeat rewrite rev_length. repeat rewrite firstn_length. - rewrite rev_length. simpl length. rewrite Hlen. + rewrite firstn_app. repeat rewrite length_rev. rewrite length_firstn. + repeat rewrite length_firstn. repeat rewrite length_skipn. + repeat rewrite length_rev. repeat rewrite length_firstn. + repeat rewrite length_rev. repeat rewrite length_firstn. + rewrite length_rev. simpl length. rewrite Hlen. rewrite (min_l c mm) by lia. rewrite (min_l (mm - kk * (mm / kk - c / kk - 1) - c) (mm-c)) by lia. 2: eauto. @@ -2430,7 +2430,7 @@ Proof. rewrite sub_add_distr. cut (c mod kk + (kk - c mod kk) mod kk <= mm - kk * (c / kk)). lia. rewrite mod_id. rewrite Heq0. rewrite <- mul_sub_distr_l. - rewrite Heq1. rewrite mul_comm. simpl. eapply le_plus_l. lia. + rewrite Heq1. rewrite mul_comm. simpl. lia. lia. unfold not. intros. eapply mod_0_iff_ceil_eq_floor_0 in H20. lia. lia. } rewrite sub_diag. rewrite add_0_l. 2: lia. @@ -2439,7 +2439,7 @@ Proof. eapply mod_0_iff_ceil_eq_floor_0 in H19. lia. lia. } rewrite add_sub. rewrite skipn_all2. rewrite firstn_nil. - 2: { rewrite rev_length. rewrite firstn_length. lia. } + 2: { rewrite length_rev. rewrite length_firstn. lia. } eauto. rewrite mul_1_r. @@ -2465,7 +2465,7 @@ Proof. rewrite sub_add_distr. cut (c mod kk + (kk - c mod kk) mod kk <= mm - kk * (c / kk)). lia. rewrite mod_id. rewrite Heq0. rewrite <- mul_sub_distr_l. - rewrite Heq1. rewrite mul_comm. simpl. eapply le_plus_l. lia. + rewrite Heq1. rewrite mul_comm. simpl. lia. lia. unfold not. intros. eapply mod_0_iff_ceil_eq_floor_0 in H20. lia. lia. } rewrite sub_diag. rewrite add_0_l. 2: lia. @@ -2489,7 +2489,7 @@ Proof. c mod kk) with 0 by lia. rewrite sub_0_r. rewrite firstn_all2 with (n:=kk). - 2: { rewrite rev_length. rewrite firstn_length. + 2: { rewrite length_rev. rewrite length_firstn. pose proof (Nat.mod_upper_bound (kk - c mod kk) kk). lia. } rewrite rev_involutive. rewrite (min_comm _ c). @@ -2500,7 +2500,7 @@ Proof. rewrite <- add_assoc. rewrite mod_id. cut (kk <= (kk *(mm/kk) - kk*(c/kk))). lia. rewrite <- mul_sub_distr_l. - rewrite Heq1. rewrite mul_comm. simpl. eapply le_plus_l. lia. + rewrite Heq1. rewrite mul_comm. simpl. lia. lia. unfold not. intros. eapply mod_0_iff_ceil_eq_floor_0 in H19. lia. lia. } 2: lia. @@ -2550,7 +2550,7 @@ Proof. erewrite map_nat_range_rec_extensionality. 2: { intros. rewrite app_comm_cons. rewrite skipn_app. rewrite firstn_app. - rewrite skipn_length. simpl length. rewrite Hlen. + rewrite length_skipn. simpl length. rewrite Hlen. replace (kk - (mm - kk * x)) with 0. 2: { rewrite (Nat.div_mod_eq mm kk). rewrite add_sub_swap . @@ -2565,14 +2565,14 @@ Proof. invert H2. remember (Z.to_nat (eval_Zexpr_Z_total $0 k)) as kk. remember (Z.to_nat (eval_Zexpr_Z_total $0 m)) as mm. - rewrite firstn_app. rewrite skipn_length. simpl length. rewrite Hlen. + rewrite firstn_app. rewrite length_skipn. simpl length. rewrite Hlen. rewrite <- map_rev. rewrite skipn_map. rewrite firstn_map. rewrite skipn_rev_nat_range_rec. rewrite firstn_rev_nat_range_rec. rewrite add_0_l. cases ((c + (kk - mm mod kk) mod kk) / kk). { simpl. rewrite min_0_l. simpl. - rewrite firstn_app. rewrite firstn_repeat. rewrite skipn_length. + rewrite firstn_app. rewrite firstn_repeat. rewrite length_skipn. simpl length. rewrite Hlen. rewrite <- mod_eq by lia. rewrite (min_l (_ mod _)). 2: { eapply mod_le. lia. } @@ -2587,7 +2587,7 @@ Proof. split. econstructor. split. { rewrite rev_app_distr. rewrite firstn_app. - rewrite rev_length. rewrite rev_repeat. rewrite repeat_length. + rewrite length_rev. rewrite rev_repeat. rewrite repeat_length. rewrite firstn_repeat. rewrite Forall_app. split. eapply Forall_repeat. eapply result_has_shape_result_shape_nat in H24. @@ -2601,8 +2601,8 @@ Proof. rewrite <- firstn_rev. simpl length. rewrite Hlen. rewrite add_sub. rewrite firstn_all2 with (n:=kk). - 2: { rewrite rev_length. rewrite firstn_length. - rewrite rev_length. simpl length. rewrite Hlen. + 2: { rewrite length_rev. rewrite length_firstn. + rewrite length_rev. simpl length. rewrite Hlen. rewrite min_l by lia. rewrite (Nat.div_mod_eq mm kk) at 1. rewrite minus_plus. pose proof (Nat.mod_upper_bound mm kk). @@ -2612,8 +2612,8 @@ Proof. lia. } split. auto. rewrite rev_app_distr. rewrite skipn_app. rewrite firstn_app. - rewrite rev_length. rewrite repeat_length. rewrite skipn_length. - rewrite rev_length. rewrite repeat_length. rewrite rev_repeat. + rewrite length_rev. rewrite repeat_length. rewrite length_skipn. + rewrite length_rev. rewrite repeat_length. rewrite rev_repeat. rewrite skipn_repeat. rewrite firstn_repeat. rewrite Forall_app. replace ((kk - mm mod kk) mod kk - (c + (kk - mm mod kk) mod kk)) @@ -2629,7 +2629,7 @@ Proof. rewrite <- firstn_rev. simpl length. rewrite Hlen. rewrite add_sub. rewrite firstn_all2 with (n:=kk). - 2: { rewrite rev_length. rewrite firstn_length. rewrite rev_length. + 2: { rewrite length_rev. rewrite length_firstn. rewrite length_rev. simpl length. rewrite Hlen. rewrite min_l by lia. rewrite (Nat.div_mod_eq mm kk) at 1. @@ -2675,17 +2675,17 @@ Proof. rewrite <- (rev_involutive (skipn _ (r0::l))). rewrite <- firstn_rev. rewrite skipn_app. rewrite firstn_app. - rewrite firstn_length. rewrite skipn_length. rewrite firstn_length. + rewrite length_firstn. rewrite length_skipn. rewrite length_firstn. simpl length. rewrite Hlen. rewrite (min_l (mm-c)) by lia. rewrite rev_app_distr. rewrite firstn_app. - rewrite rev_length. rewrite firstn_length. rewrite skipn_length. - rewrite rev_length. + rewrite length_rev. rewrite length_firstn. rewrite length_skipn. + rewrite length_rev. rewrite Forall_app. split. { eapply forall_firstn. eapply Forall_rev. eapply forall_firstn. eapply forall_skipn. eapply Forall_rev. rewrite gen_pad_filter_until_0. rewrite <- H20. rewrite <- gen_pad_filter_until_0. eauto. } - rewrite firstn_length. rewrite rev_length. simpl length. + rewrite length_firstn. rewrite length_rev. simpl length. rewrite Hlen. rewrite (min_l c mm) by lia. repeat rewrite <- sub_add_distr. rewrite sub_add by lia. repeat rewrite sub_add_distr. @@ -2813,8 +2813,7 @@ Proof. rewrite (Nat.add_comm n5). rewrite sub_add_distr. rewrite (sub_sub_distr n4). - 2: { rewrite Heqn4. rewrite Heq2. rewrite mul_comm. simpl. - eapply le_plus_l. } + 2: { rewrite Heqn4. rewrite Heq2. rewrite mul_comm. simpl. lia. } rewrite sub_diag. simpl. rewrite sub_sub_distr. 2: { pose proof (Nat.mod_upper_bound c kk). lia. } @@ -2831,7 +2830,7 @@ Proof. rewrite mod_mod. 2: lia. replace (kk - mm mod kk) with ((kk - c mod kk) mod kk + (kk - mm mod kk - ((kk - c mod kk) mod kk))). - 2: { rewrite <- le_plus_minus. lia. + 2: { rewrite add_sub_assoc. lia. pose proof (mod_id c kk). pose proof (mod_id mm kk). lia. } rewrite add_assoc. rewrite mod_id. @@ -2857,16 +2856,16 @@ Proof. rewrite <- (firstn_skipn (length (r0::l) - c) (r0::l)). rewrite <- (rev_involutive (firstn _ (r0::l))). rewrite <- skipn_rev. - rewrite skipn_app. rewrite firstn_app. rewrite skipn_length. - rewrite rev_length. rewrite skipn_length. - rewrite rev_length. + rewrite skipn_app. rewrite firstn_app. rewrite length_skipn. + rewrite length_rev. rewrite length_skipn. + rewrite length_rev. simpl length. rewrite Hlen. rewrite rev_app_distr. rewrite skipn_app. - rewrite rev_length. rewrite firstn_length. - rewrite skipn_length. rewrite skipn_length. simpl length. + rewrite length_rev. rewrite length_firstn. + rewrite length_skipn. rewrite length_skipn. simpl length. rewrite Hlen. rewrite firstn_app. - rewrite skipn_length. rewrite rev_length. rewrite firstn_length. - rewrite skipn_length. rewrite skipn_length. + rewrite length_skipn. rewrite length_rev. rewrite length_firstn. + rewrite length_skipn. rewrite length_skipn. simpl length. rewrite Hlen. rewrite (sub_sub_distr mm mm c). 2: { lia. } @@ -2919,8 +2918,8 @@ Proof. assert (c mod kk < mm mod kk \/ mm mod kk < c mod kk) by lia. cases H22. - rewrite skipn_all2. rewrite firstn_nil. econstructor. - rewrite rev_length. rewrite firstn_length. - rewrite skipn_length. simpl length. rewrite H21. + rewrite length_rev. rewrite length_firstn. + rewrite length_skipn. simpl length. rewrite H21. rewrite (sub_sub_distr mm mm c) by lia. rewrite sub_diag. rewrite add_0_l. rewrite (Nat.div_mod_eq c kk) at 2. @@ -2957,8 +2956,7 @@ Proof. rewrite sub_0_r in *. eapply div_small_iff in Heq2. rewrite (mod_small mm kk) in * by lia. lia. lia. lia. } rewrite (Nat.div_mod_eq c kk) at 2. - rewrite min_l. - 2: { eapply plus_le_compat_r. lia. } + rewrite min_l by lia. rewrite <- (mod_small (kk - mm mod kk + c mod kk) kk). 2: { rewrite <- (mod_id mm kk) at 4 by lia. rewrite (mod_small (kk - mm mod kk) kk) by lia. @@ -3035,7 +3033,7 @@ Proof. rewrite (Nat.add_comm (_ - _) (_ - _)). rewrite sub_add_distr. rewrite (sub_sub_distr _ _ kk). - 2: { rewrite Heq2. rewrite mul_comm. simpl. eapply le_plus_l. } + 2: { rewrite Heq2. rewrite mul_comm. simpl. lia. } 2: lia. rewrite sub_diag. simpl. rewrite sub_sub_distr. @@ -3043,8 +3041,8 @@ Proof. rewrite sub_diag. simpl. rewrite mod_mod. rewrite skipn_all2. rewrite firstn_nil. econstructor. - rewrite rev_length. rewrite firstn_length. - rewrite skipn_length. simpl length. rewrite H21. + rewrite length_rev. rewrite length_firstn. + rewrite length_skipn. simpl length. rewrite H21. rewrite sub_sub_distr by lia. rewrite sub_diag. simpl. rewrite min_l. 2: { pose proof (mod_le c kk). lia. } @@ -3053,7 +3051,7 @@ Proof. rewrite (mod_small (kk - mm mod kk)) by lia. replace (kk - mm mod kk) with (kk - c mod kk + (kk - mm mod kk - (kk - c mod kk))). - 2: { rewrite le_plus_minus_r. lia. lia. } + 2: { lia. } rewrite (Nat.add_comm). repeat rewrite add_assoc. rewrite <- (mod_small (kk - c mod kk) kk) at 1 by lia. @@ -3100,8 +3098,8 @@ Proof. rewrite rev_involutive. rewrite skipn_skipn. rewrite firstn_skipn_comm. rewrite firstn_firstn. - rewrite firstn_length. rewrite skipn_length. - rewrite rev_length. simpl length. rewrite H21. + rewrite length_firstn. rewrite length_skipn. + rewrite length_rev. simpl length. rewrite H21. rewrite (min_l (mm - c - _) (mm-c)). 2: eapply le_sub_l. cases (c / kk). eapply div_small_iff in Heq2. rewrite mod_small in H22 by lia. lia. @@ -3220,8 +3218,8 @@ Proof. rewrite (mod_small mm kk) in * by lia. lia. lia. rewrite (min_l kk c) by lia. rewrite firstn_rev. - rewrite rev_involutive. rewrite skipn_length. - rewrite app_length. rewrite rev_length. simpl. + rewrite rev_involutive. rewrite length_skipn. + rewrite length_app. rewrite length_rev. simpl. rewrite add_succ_r. rewrite add_0_r. rewrite H21. replace (mm - c - kk) with 0. 2: { rewrite (Nat.div_mod_eq mm kk). @@ -3257,12 +3255,12 @@ Proof. rewrite <- sub_sub_distr. 2: { lia. } 2: { rewrite <- mul_sub_distr_l. rewrite Heq2. - rewrite mul_comm. simpl . eapply le_plus_l. } + rewrite mul_comm. simpl. lia. } lia. } rewrite <- mul_sub_distr_l. repeat rewrite sub_add_distr. rewrite (sub_sub_distr _ _ kk). - 2: { rewrite Heq2. rewrite mul_comm. simpl. eapply le_plus_l. } + 2: { rewrite Heq2. rewrite mul_comm. simpl. lia. } 2: lia. rewrite sub_diag. simpl. rewrite (sub_sub_distr kk kk). 2: { pose proof (Nat.mod_upper_bound c kk). lia. } @@ -3274,8 +3272,8 @@ Proof. rewrite firstn_rev. rewrite rev_involutive. rewrite skipn_skipn. rewrite firstn_skipn_comm. rewrite firstn_firstn. - rewrite firstn_length. rewrite skipn_length. rewrite app_length. - rewrite rev_length. simpl. rewrite add_succ_r. rewrite add_0_r. + rewrite length_firstn. rewrite length_skipn. rewrite length_app. + rewrite length_rev. simpl. rewrite add_succ_r. rewrite add_0_r. rewrite H21. rewrite (min_l _ (mm -c)) by lia. replace (mm - c) with (kk * (mm /kk) + mm mod kk - (kk *(c/kk) + c mod kk)). @@ -3289,7 +3287,7 @@ Proof. eapply forall_skipn. rewrite <- sub_add_distr. rewrite sub_add. - 2: { rewrite Heq2. rewrite mul_comm. simpl. eapply le_plus_l. } + 2: { rewrite Heq2. rewrite mul_comm. simpl. lia. } replace (kk * (mm / kk - c / kk) + mm mod kk - c mod kk - kk * (mm / kk - c / kk)) with 0. 2: { symmetry. eapply sub_0_le. rewrite add_sub_swap. @@ -3333,7 +3331,7 @@ Proof. rewrite (Nat.add_comm (c mod kk)). rewrite sub_add_distr. rewrite (sub_sub_distr _ _ kk). - 2: { rewrite Heq2. rewrite mul_comm. simpl. eapply le_plus_l. } + 2: { rewrite Heq2. rewrite mul_comm. simpl. lia. } 2: { lia. } rewrite minus_plus. remember ((kk - mm mod kk - (kk - c mod kk)) mod kk) as XX. @@ -3348,9 +3346,7 @@ Proof. rewrite mod_id by lia. rewrite sub_diag. reflexivity. } rewrite H23. rewrite add_0_l. rewrite HeqX, HeqXX, HeqXXX. - lia. - rewrite le_plus_minus_r. reflexivity. - lia. + lia. lia. } } @@ -3479,7 +3475,7 @@ Proof. eapply constant_nonneg_bounds_size_of_eval_expr_result_has_shape. eauto. eauto. eauto. eauto. * rewrite firstn_app. - rewrite app_length. rewrite rev_length. simpl. + rewrite length_app. rewrite length_rev. simpl. eapply Forall_app. propositional. cases (c - (Datatypes.length l + 1)). simpl in *. econstructor. simpl. rewrite firstn_nil. econstructor. 2: eauto. @@ -3493,15 +3489,15 @@ Proof. eauto. eauto. eauto. * posnats. pose proof H24. rewrite skipn_app in *. - rewrite firstn_app in *. rewrite skipn_length in *. - rewrite rev_length in *. + rewrite firstn_app in *. rewrite length_skipn in *. + rewrite length_rev in *. eapply Forall_app in H29. invs. repeat erewrite Forall_app. rewrite skipn_app. rewrite firstn_app. rewrite Forall_app. - rewrite skipn_length. rewrite rev_length. + rewrite length_skipn. rewrite length_rev. split. split. auto. eauto. - repeat rewrite app_length. repeat rewrite rev_length. + repeat rewrite length_app. repeat rewrite length_rev. simpl. cases (c - (Datatypes.length l + 1)). simpl. 2: { simpl. rewrite skipn_nil. rewrite firstn_nil. eauto. } @@ -3526,7 +3522,7 @@ Proof. cases ll. { simpl. split. auto. - rewrite firstn_app. rewrite rev_length. + rewrite firstn_app. rewrite length_rev. cases (rr - length l). - simpl. rewrite app_nil_r. pose proof Hsh' as HH. @@ -3599,9 +3595,9 @@ Proof. simpl. rewrite firstn_nil. simpl in HH. invs. rewrite Forall_app. split. rewrite firstn_all2. - 2: { rewrite rev_length. lia. } + 2: { rewrite length_rev. lia. } rewrite firstn_all2 in H20. - 2: { rewrite rev_length. lia. } + 2: { rewrite length_rev. lia. } eauto. econstructor; eauto. } simpl. split. econstructor. @@ -3644,7 +3640,7 @@ Proof. 2: { econstructor. eauto. } simpl in Hsh'. invs. eauto. - rewrite firstn_app. rewrite rev_length. + rewrite firstn_app. rewrite length_rev. eapply IHeval_expr2 with (pads:= PadCons 0 ll @@ -3781,13 +3777,13 @@ Proof. 2: { simpl. rewrite H. reflexivity. } 2: { rewrite H0. reflexivity. } rewrite firstn_all2 in H18. - 2: { rewrite app_length. rewrite rev_length. simpl in *. lia. } + 2: { rewrite length_app. rewrite length_rev. simpl in *. lia. } eapply Forall_app in H18. invs. simpl rev. repeat rewrite skipn_app. repeat rewrite firstn_app. - repeat rewrite app_length. repeat rewrite skipn_length. - repeat rewrite rev_length. + repeat rewrite length_app. repeat rewrite length_skipn. + repeat rewrite length_rev. repeat rewrite Forall_app. repeat rewrite sub_add_distr in *. split. split. split. eapply forall_firstn. eauto. @@ -3808,7 +3804,7 @@ Proof. Z.to_nat (eval_Zexpr_Z_total $0 hi - eval_Zexpr_Z_total $0 lo - 1) -1) by lia. rewrite skipn_all2. - 2: { rewrite rev_length. lia. } + 2: { rewrite length_rev. lia. } rewrite firstn_nil. replace (Datatypes.length l - Datatypes.S n) with 0 by lia. rewrite sub_0_r. @@ -3826,7 +3822,7 @@ Proof. eapply length_eval_expr_gen in H8. 2: { simpl. rewrite H,H0. reflexivity. } rewrite skipn_app. repeat rewrite firstn_app. - rewrite skipn_length. rewrite rev_length. + rewrite length_skipn. rewrite length_rev. cases (c - length l). - simpl. rewrite app_nil_r. simpl in H23. rewrite Z.sub_0_r in H23. @@ -3868,7 +3864,7 @@ Proof. split. eauto. eauto. + simpl. rewrite firstn_nil. rewrite firstn_all2 with (n:=rr). - 2: { rewrite skipn_length. rewrite rev_length. lia. } + 2: { rewrite length_skipn. rewrite length_rev. lia. } rewrite <- H8 in *. eapply IHeval_expr2 in Hsh'. 2: { invert H6. invert H7. @@ -3903,7 +3899,7 @@ Proof. split. eauto. split. eauto. rewrite Forall_app. split. auto. rewrite firstn_all2 in H23. - 2: { rewrite skipn_length. rewrite rev_length. + 2: { rewrite length_skipn. rewrite length_rev. rewrite H8. lia. } eauto. eauto. econstructor. 2: eauto. @@ -3962,9 +3958,9 @@ Proof. simpl in Hsh'. invs. split. eauto. rewrite firstn_app in *. - repeat rewrite rev_length in *. simpl length. + repeat rewrite length_rev in *. simpl length. simpl rev. rewrite firstn_app. - rewrite rev_length. + rewrite length_rev. eapply Forall_app in H18. invs. repeat rewrite Forall_app. split. split. eauto. eauto. @@ -3986,7 +3982,7 @@ Proof. rewrite skipn_app. rewrite firstn_app. rewrite Forall_app. split. eauto. - rewrite skipn_length. rewrite app_length. rewrite rev_length. + rewrite length_skipn. rewrite length_app. rewrite length_rev. simpl. replace (c - (Datatypes.length l + 1)) with 0 by lia. simpl. @@ -4224,7 +4220,7 @@ Proof. eauto. eapply constant_nonneg_bounds_size_of_eval_expr_result_has_shape in Hsh2'; eauto. - eapply result_has_shape_length in Hsh. rewrite app_length in *. + eapply result_has_shape_length in Hsh. rewrite length_app in *. pose proof Hsh1' as Hsh1''. pose proof Hsh2' as Hsh2''. pose proof Hsh' as HH. pose proof Hsh'' as HHH. eapply result_has_shape_result_shape_nat in HH,HHH,Hsh1'',Hsh2''. @@ -4324,7 +4320,7 @@ Proof. rewrite <- gen_pad_filter_until_0. auto. rewrite rev_app_distr. rewrite firstn_app. - rewrite rev_length. + rewrite length_rev. replace (b - Datatypes.length (r0 :: l2)) with 0 by lia. split. simpl. rewrite app_nil_r. eapply Forall_forall. intros. eapply Forall_forall in H2. @@ -4334,7 +4330,7 @@ Proof. rewrite <- gen_pad_filter_until_0. auto. rewrite skipn_app. rewrite firstn_app. - rewrite skipn_length. + rewrite length_skipn. replace (l4 - (Datatypes.length (r :: l1) - x)) with 0 by lia. split. simpl. rewrite app_nil_r. eapply Forall_forall. intros. eapply Forall_forall in H18. @@ -4358,7 +4354,7 @@ Proof. eauto. rewrite skipn_app. rewrite firstn_app. - rewrite skipn_length. rewrite rev_length. + rewrite length_skipn. rewrite length_rev. replace (r2 - (Datatypes.length (r0 :: l2) - b)) with 0 by lia. simpl firstn at 2. rewrite app_nil_r. simpl. @@ -4480,17 +4476,17 @@ Proof. 2: { eapply forall_result_has_shape. eapply forall_firstn. econstructor. eauto. eauto. - rewrite firstn_length. reflexivity. } + rewrite length_firstn. reflexivity. } 2: { eapply forall_result_has_shape. eapply forall_skipn. econstructor. eauto. eauto. - rewrite skipn_length. reflexivity. } + rewrite length_skipn. reflexivity. } 2: lia. erewrite forall_gen_pad_get_col. 2: { eauto. } 2: lia. - rewrite firstn_length. + rewrite length_firstn. rewrite firstn_rev in H7. pose proof H7. eapply Forall_rev in H4. rewrite rev_involutive in H4. @@ -4498,19 +4494,19 @@ Proof. erewrite <- (firstn_skipn (Datatypes.S (Datatypes.length l) - y) (r0::l)). rewrite skipn_app. - rewrite firstn_length. rewrite skipn_skipn. + rewrite length_firstn. rewrite skipn_skipn. erewrite get_col_app. 2: { eapply forall_result_has_shape. eapply forall_skipn. eapply forall_firstn. econstructor; eauto. - rewrite skipn_length. rewrite firstn_length. simpl length. + rewrite length_skipn. rewrite length_firstn. simpl length. replace (min (Datatypes.S (length l) - y) (Datatypes.S (length l))) with ((Datatypes.S (length l)) - y) by lia. reflexivity. } 2: { eapply forall_result_has_shape. eapply forall_skipn. econstructor; eauto. - rewrite skipn_length. simpl length. + rewrite length_skipn. simpl length. replace (min (Datatypes.S (length l) - y) (Datatypes.S (length l))) with ((Datatypes.S (length l)) - y) by lia. @@ -4528,7 +4524,7 @@ Proof. cases (x - (Datatypes.S (Datatypes.length l) - y)). lia. lia. } 2: lia. - rewrite skipn_length. simpl length. + rewrite length_skipn. simpl length. replace (x - (Datatypes.S (Datatypes.length l) - y)) with 0 by lia. rewrite add_0_l. replace (Datatypes.S (length l) - (Datatypes.S (length l) - y)) @@ -4541,7 +4537,7 @@ Proof. rewrite <- (firstn_skipn r (skipn y (rev (r0 :: l)))). rewrite rev_app_distr. rewrite skipn_app. - rewrite rev_length. repeat rewrite skipn_length. rewrite rev_length. + rewrite length_rev. repeat rewrite length_skipn. rewrite length_rev. simpl length. replace (min x (Datatypes.S (Datatypes.length l))) with x by lia. erewrite get_col_app. @@ -4549,38 +4545,38 @@ Proof. eapply forall_skipn. eapply Forall_rev. eapply forall_skipn. eapply forall_skipn. eapply Forall_rev. econstructor; eauto. - rewrite skipn_length. rewrite rev_length. - repeat rewrite skipn_length. rewrite rev_length. reflexivity. } + rewrite length_skipn. rewrite length_rev. + repeat rewrite length_skipn. rewrite length_rev. reflexivity. } 2: { eapply forall_result_has_shape. eapply forall_skipn. eapply Forall_rev. eapply forall_firstn. eapply forall_skipn. eapply Forall_rev. econstructor; eauto. - rewrite skipn_length. rewrite rev_length. - rewrite firstn_length. rewrite skipn_length. - rewrite rev_length. reflexivity. } + rewrite length_skipn. rewrite length_rev. + rewrite length_firstn. rewrite length_skipn. + rewrite length_rev. reflexivity. } 2: { lia. } erewrite <- (skipn_get_col (rev (firstn r (skipn y (rev (r0 :: l)))))). 2: { eapply result_has_shape_rev. eapply forall_result_has_shape. eapply forall_firstn. eapply forall_skipn. eapply Forall_rev. econstructor; eauto. - rewrite firstn_length. rewrite skipn_length. - rewrite rev_length. simpl. reflexivity. } + rewrite length_firstn. rewrite length_skipn. + rewrite length_rev. simpl. reflexivity. } pose proof H10. eapply Forall_rev in H4. erewrite (forall_get_col_relate_pads_gen_pad (rev (firstn r (skipn y (rev (r0 :: l)))))). 4: { eapply forall_result_has_shape. eapply Forall_rev. eapply forall_firstn. eapply forall_skipn. eapply Forall_rev. econstructor; eauto. - rewrite rev_length. rewrite firstn_length. rewrite skipn_length. - rewrite rev_length. simpl length. reflexivity. } + rewrite length_rev. rewrite length_firstn. rewrite length_skipn. + rewrite length_rev. simpl length. reflexivity. } 2: { eapply Forall_impl. 2: { eapply H4. } simpl. intros. cases a0. propositional. invs. eassumption. } 2: lia. - rewrite rev_length. rewrite firstn_length. rewrite skipn_length. - rewrite rev_length. simpl length. + rewrite length_rev. rewrite length_firstn. rewrite length_skipn. + rewrite length_rev. simpl length. remember (Init.Nat.min r (Datatypes.S (Datatypes.length l) - y)). simpl gen_pad_list at 2. rewrite skipn_repeat. @@ -4593,13 +4589,13 @@ Proof. rewrite skipn_skipn. rewrite <- rev_skipn_rev_skipn. rewrite skipn_rev. rewrite rev_involutive. - rewrite skipn_length. + rewrite length_skipn. rewrite sub_add_distr. simpl length. erewrite forall_get_col_relate_pads_gen_pad. 4: { eapply forall_result_has_shape. eapply forall_firstn. eapply forall_skipn. econstructor; eauto. - rewrite firstn_length. rewrite skipn_length. simpl length. + rewrite length_firstn. rewrite length_skipn. simpl length. rewrite min_l. reflexivity. lia. } 2: { eapply forall_firstn_ge. @@ -4607,7 +4603,7 @@ Proof. simpl. intros. cases a0. propositional. invs. eassumption. lia. } - rewrite firstn_length. rewrite skipn_length. + rewrite length_firstn. rewrite length_skipn. remember (Init.Nat.min (Datatypes.S (Datatypes.length l) - x - r - y) (Datatypes.length (r0 :: l) - x)). simpl (gen_pad_list (_::_)). @@ -4638,12 +4634,10 @@ Proof. rewrite sub_add by auto. rewrite <- sub_add_distr. rewrite Nat.add_comm. - rewrite add_assoc. - rewrite le_plus_minus_r. reflexivity. + rewrite add_assoc. rewrite add_sub_assoc, minus_plus. reflexivity. rewrite Nat.add_comm. rewrite H9. auto. + rewrite <- Heq0. - rewrite (not_le_minus_0 _ x). - 2: { lia. } + replace (_ - x) with 0 by lia. rewrite add_0_l. rewrite add_sub_swap. replace (x - (x - (Datatypes.S (Datatypes.length l) - y - r))) with ((Datatypes.S (Datatypes.length l) - y - r)). @@ -4655,8 +4649,7 @@ Proof. lia. eapply le_sub_l. - rewrite min_r by lia. - rewrite (not_le_minus_0 _ r). - 2: { lia. } + replace (_ - r) with 0 by lia. rewrite sub_0_r. rewrite sub_0_l. rewrite add_0_l. rewrite minus_plus. rewrite sub_add. reflexivity. @@ -4676,35 +4669,35 @@ Proof. erewrite get_col_app with (b:=(Z.to_nat (eval_Zexpr_Z_total $0 m1))). 2: { eapply result_has_shape_map_rev. eapply forall_result_has_shape. eapply forall_firstn. - econstructor; eauto. rewrite firstn_length. reflexivity. } + econstructor; eauto. rewrite length_firstn. reflexivity. } 2: { eapply result_has_shape_map_rev. eapply forall_result_has_shape. eapply forall_skipn. - econstructor; eauto. rewrite skipn_length. reflexivity. } + econstructor; eauto. rewrite length_skipn. reflexivity. } 2: { lia. } erewrite forall_gen_pad_get_col. 2: { eapply Forall_map. eapply Forall_impl. 2: eassumption. simpl. intros. subst. erewrite rev_repeat. reflexivity. } - rewrite map_length. rewrite firstn_length. + rewrite length_map. rewrite length_firstn. rewrite min_l. 2: { simpl. lia. } rewrite <- (rev_involutive (r0::l)). rewrite <- (firstn_skipn y (rev (r0::l))). rewrite rev_app_distr. rewrite skipn_app. rewrite map_app. - rewrite rev_length. rewrite skipn_length. rewrite rev_length. + rewrite length_rev. rewrite length_skipn. rewrite length_rev. erewrite get_col_app with (b:=(Z.to_nat (eval_Zexpr_Z_total $0 m1))). 2: { eapply result_has_shape_map_rev. eapply forall_result_has_shape. eapply forall_skipn. eapply Forall_rev. eapply forall_skipn. eapply Forall_rev. - econstructor; eauto. rewrite skipn_length. - rewrite rev_length. rewrite skipn_length. rewrite rev_length. + econstructor; eauto. rewrite length_skipn. + rewrite length_rev. rewrite length_skipn. rewrite length_rev. reflexivity. } 2: { eapply result_has_shape_map_rev. eapply forall_result_has_shape. eapply forall_skipn. eapply Forall_rev. eapply forall_firstn. eapply Forall_rev. - econstructor; eauto. rewrite skipn_length. - rewrite rev_length. rewrite firstn_length. rewrite rev_length. + econstructor; eauto. rewrite length_skipn. + rewrite length_rev. rewrite length_firstn. rewrite length_rev. reflexivity. } 2: lia. erewrite (forall_gen_pad_get_col (map (fun x1 : result => match x1 with @@ -4719,8 +4712,8 @@ Proof. reflexivity. } 2: lia. 2: lia. - rewrite map_length. rewrite skipn_length. - rewrite rev_length. rewrite firstn_length. rewrite rev_length. + rewrite length_map. rewrite length_skipn. + rewrite length_rev. rewrite length_firstn. rewrite length_rev. rewrite min_l. 2: simpl; lia. simpl length. pose proof H12. rewrite H9. @@ -4736,20 +4729,20 @@ Proof. eapply forall_result_has_shape. eapply forall_skipn. eapply Forall_rev. eapply forall_skipn. eapply forall_skipn. eapply Forall_rev. - econstructor; eauto. rewrite skipn_length. - rewrite rev_length. repeat rewrite skipn_length. - rewrite rev_length. reflexivity. } + econstructor; eauto. rewrite length_skipn. + rewrite length_rev. repeat rewrite length_skipn. + rewrite length_rev. reflexivity. } 2: { eapply result_has_shape_map_rev. eapply forall_result_has_shape. eapply forall_skipn. eapply Forall_rev. eapply forall_firstn. eapply forall_skipn. eapply Forall_rev. - econstructor; eauto. rewrite skipn_length. - repeat rewrite rev_length. repeat rewrite skipn_length. - rewrite firstn_length. rewrite skipn_length. - rewrite rev_length. reflexivity. } + econstructor; eauto. rewrite length_skipn. + repeat rewrite length_rev. repeat rewrite length_skipn. + rewrite length_firstn. rewrite length_skipn. + rewrite length_rev. reflexivity. } 2: lia. - rewrite rev_length. repeat rewrite skipn_length. rewrite rev_length. + rewrite length_rev. repeat rewrite length_skipn. rewrite length_rev. simpl length. erewrite (forall_get_col_relate_pads_gen_pad (map (fun x1 : result => match x1 with @@ -4769,17 +4762,17 @@ Proof. eapply forall_result_has_shape. eapply forall_skipn. eapply Forall_rev. eapply forall_firstn. eapply forall_skipn. eapply Forall_rev. econstructor; eauto. - rewrite skipn_length. rewrite rev_length. - rewrite firstn_length. rewrite skipn_length. rewrite rev_length. + rewrite length_skipn. rewrite length_rev. + rewrite length_firstn. rewrite length_skipn. rewrite length_rev. reflexivity. } - rewrite map_length. rewrite skipn_length. - rewrite rev_length. rewrite firstn_length. rewrite skipn_length. - rewrite rev_length. simpl length. + rewrite length_map. rewrite length_skipn. + rewrite length_rev. rewrite length_firstn. rewrite length_skipn. + rewrite length_rev. simpl length. rewrite skipn_skipn. rewrite <- rev_skipn_rev_skipn. rewrite skipn_rev. rewrite rev_involutive. - rewrite skipn_length. simpl length. + rewrite length_skipn. simpl length. pose proof H5. erewrite forall_get_col_relate_pads_gen_pad @@ -4794,8 +4787,8 @@ Proof. eapply le_sub_le_add_r. lia. } 2: { lia. } - rewrite map_length. rewrite firstn_length. - rewrite skipn_length. simpl length. + rewrite length_map. rewrite length_firstn. + rewrite length_skipn. simpl length. remember (Init.Nat.min (Datatypes.S (Datatypes.length l) - x - (r + y)) (Datatypes.S (Datatypes.length l) - x)). remember (Init.Nat.min r (Datatypes.S (Datatypes.length l) - y) - @@ -4810,62 +4803,12 @@ Proof. rewrite min_l. 2: { eapply le_sub_l. } - cases (Datatypes.S (Datatypes.length l) - y - r). - - rewrite sub_0_r. rewrite min_r. - 2: { lia. } - repeat rewrite <- sub_add_distr. - rewrite (Nat.add_comm r y). repeat rewrite add_assoc. - rewrite (sub_add_distr _ _ r). rewrite (Nat.add_comm y x). - rewrite <- (add_assoc x). - rewrite Nat.add_comm. rewrite add_assoc. rewrite (Nat.add_comm y x). - rewrite (Nat.add_comm (_ - _ - _)). - rewrite add_assoc. - rewrite le_plus_minus_r. - 2: { eauto. } - rewrite <- sub_add_distr. - rewrite <- (add_assoc x y r). - rewrite (Nat.add_comm x). - repeat rewrite sub_add_distr. - rewrite Heq0. rewrite sub_0_l. rewrite add_0_r. reflexivity. - - rewrite min_l. - 2: { lia. } - rewrite <- Heq0. repeat rewrite add_assoc. - rewrite <- sub_add_distr. - rewrite (Nat.add_comm r y). rewrite add_assoc. - rewrite sub_add_distr. - rewrite (Nat.add_comm _ y). - repeat rewrite add_assoc. - rewrite (Nat.add_comm y). - rewrite add_sub_assoc. - 2: { lia. } - rewrite <- add_assoc. - cases (Datatypes.S (length l) - (x + y) - r). - + rewrite add_0_l. - rewrite <- sub_add_distr. - rewrite <- sub_add_distr in Heq1. - rewrite <- add_assoc in Heq1. - rewrite Nat.add_comm in Heq1. - rewrite sub_add_distr in Heq1. - rewrite <- add_assoc. - rewrite add_sub_swap. - 2: { eapply le_sub_l. } - lia. - + rewrite <- Heq1. - rewrite sub_add. - 2: { lia. } - rewrite le_plus_minus_r. - 2: { lia. } - rewrite <- sub_add_distr in Heq1. - rewrite <- add_assoc in Heq1. - rewrite Nat.add_comm in Heq1. - rewrite sub_add_distr in Heq1. - rewrite (not_le_minus_0 x). - 2: { lia. } - rewrite sub_0_r. reflexivity. - - eapply result_has_shape_map_rev. - eapply forall_result_has_shape. eapply forall_firstn. - eapply forall_skipn. econstructor; eauto. - rewrite firstn_length. rewrite skipn_length. reflexivity. } + clear -H12. lia. + + eapply result_has_shape_map_rev. + eapply forall_result_has_shape. eapply forall_firstn. + eapply forall_skipn. econstructor; eauto. + rewrite length_firstn. rewrite length_skipn. reflexivity. } erewrite skipn_transpose_result_list. 2: { econstructor; eauto. } @@ -4924,7 +4867,7 @@ Proof. 2: { eapply result_has_shape_map_rev. econstructor; eauto. } rewrite firstn_map. erewrite forall_gen_pad_get_col. - rewrite map_length. + rewrite length_map. 2: { eapply Forall_map. eapply Forall_impl. 2: eassumption. simpl. intros. subst. rewrite <- repeat_cons. rewrite rev_repeat. reflexivity. } @@ -5057,24 +5000,24 @@ Proof. erewrite firstn_get_col. 2: { eapply forall_result_has_shape. eapply forall_skipn. econstructor; eauto. - rewrite skipn_length. reflexivity. } + rewrite length_skipn. reflexivity. } erewrite firstn_get_col. 2: { eapply forall_result_has_shape. eapply forall_skipn. eapply Forall_rev. econstructor; eauto. - rewrite skipn_length. rewrite rev_length. reflexivity. } + rewrite length_skipn. rewrite length_rev. reflexivity. } erewrite forall_get_col_relate_pads_gen_pad. 2: { eapply Forall_impl. 2: eassumption. simpl. intros. cases a0. propositional. invs. eassumption. } 3: { eapply forall_result_has_shape. eapply forall_firstn. eapply forall_skipn. econstructor. eauto. eauto. - rewrite firstn_length. rewrite skipn_length. reflexivity. } + rewrite length_firstn. rewrite length_skipn. reflexivity. } 2: { lia. } erewrite forall_get_col_relate_pads_gen_pad. 2: { eapply Forall_impl. 2: eassumption. simpl. intros. cases a0. propositional. invs. eassumption. } 3: { eapply forall_result_has_shape. eapply forall_firstn. eapply forall_skipn. eapply Forall_rev. econstructor. eauto. eauto. - rewrite firstn_length. rewrite skipn_length. rewrite rev_length. + rewrite length_firstn. rewrite length_skipn. rewrite length_rev. reflexivity. } 2: { lia. } rewrite gen_pad_filter_until_0. rewrite H10. @@ -5097,18 +5040,18 @@ Proof. repeat erewrite get_col_app. 2: { eapply forall_result_has_shape. eapply forall_firstn. eapply Forall_rev. econstructor; eauto. - rewrite firstn_length. rewrite rev_length. reflexivity. } + rewrite length_firstn. rewrite length_rev. reflexivity. } 2: { eapply forall_result_has_shape. eapply forall_firstn. eapply forall_skipn. eapply Forall_rev. econstructor; eauto. - rewrite firstn_length. erewrite skipn_length. rewrite rev_length. + rewrite length_firstn. erewrite length_skipn. rewrite length_rev. reflexivity. } 2: { lia. } 2: { eapply forall_result_has_shape. eapply forall_firstn. - econstructor; eauto. rewrite firstn_length. reflexivity. } + econstructor; eauto. rewrite length_firstn. reflexivity. } 2: { eapply forall_result_has_shape. eapply forall_firstn. eapply forall_skipn. - econstructor; eauto. rewrite firstn_length. - rewrite skipn_length. reflexivity. } + econstructor; eauto. rewrite length_firstn. + rewrite length_skipn. reflexivity. } 2: lia. repeat rewrite Forall_app. @@ -5122,14 +5065,14 @@ Proof. erewrite get_col_rev. 2: { eapply forall_result_has_shape. eapply forall_firstn. eapply forall_skipn. - econstructor; eauto. rewrite firstn_length. rewrite skipn_length. + econstructor; eauto. rewrite length_firstn. rewrite length_skipn. reflexivity. } 2: lia. erewrite get_col_rev. 2: { eapply forall_result_has_shape. eapply forall_firstn. eapply forall_skipn. eapply Forall_rev. - econstructor; eauto. rewrite firstn_length. rewrite skipn_length. - rewrite rev_length. reflexivity. } + econstructor; eauto. rewrite length_firstn. rewrite length_skipn. + rewrite length_rev. reflexivity. } 2: lia. erewrite forall_get_col_relate_pads_gen_pad. @@ -5138,8 +5081,8 @@ Proof. cases a0. propositional. invs. eassumption. } 3: { eapply result_has_shape_map_rev. eapply forall_result_has_shape. eapply forall_firstn. eapply forall_skipn. - econstructor; eauto. rewrite firstn_length. - rewrite skipn_length. reflexivity. } + econstructor; eauto. rewrite length_firstn. + rewrite length_skipn. reflexivity. } 2: { lia. } erewrite forall_get_col_relate_pads_gen_pad. 2: { eapply Forall_map. @@ -5148,8 +5091,8 @@ Proof. 3: { eapply result_has_shape_map_rev. eapply forall_result_has_shape. eapply forall_firstn. eapply forall_skipn. eapply Forall_rev. - econstructor; eauto. rewrite firstn_length. - rewrite skipn_length. rewrite rev_length. reflexivity. } + econstructor; eauto. rewrite length_firstn. + rewrite length_skipn. rewrite length_rev. reflexivity. } 2: { lia. } rewrite gen_pad_filter_until_0. rewrite H10. @@ -5191,7 +5134,7 @@ Proof. { simpl in *. pose proof (truncl_list_length_empty (Z.to_nat (eval_Zexpr_Z_total $0 k)) (rev l)). - rewrite rev_length in *. + rewrite length_rev in *. erewrite result_has_shape_length in H6. 2: { eauto. } assert (Z.to_nat (eval_Zexpr_Z_total $0 m) <= @@ -5204,7 +5147,7 @@ Proof. { simpl in *. pose proof (truncl_list_length_empty (Z.to_nat (eval_Zexpr_Z_total $0 k)) (rev l)). - rewrite rev_length in *. + rewrite length_rev in *. erewrite result_has_shape_length in H6. 2: { eauto. } assert (Z.to_nat (eval_Zexpr_Z_total $0 m) <= @@ -5237,8 +5180,8 @@ Proof. with (n:=(Z.to_nat (eval_Zexpr_Z_total $0 k))) (l:=rev l) in H10. rewrite rev_app_distr in H10. rewrite skipn_app in H10. rewrite firstn_app in H10. - rewrite skipn_length in H10. rewrite rev_length in H10. - rewrite skipn_length in H10. rewrite rev_length in H10. + rewrite length_skipn in H10. rewrite length_rev in H10. + rewrite length_skipn in H10. rewrite length_rev in H10. eapply Forall_app in H10. invs. eapply Forall_forall. intros. eapply Forall_forall in H12. 2: eauto. @@ -5363,8 +5306,8 @@ Proof. with (l:=l) (n:=(Z.to_nat (eval_Zexpr_Z_total $0 k))) in H13. rewrite rev_app_distr in *. rewrite skipn_app in *. rewrite firstn_app in *. - rewrite skipn_length in *. rewrite rev_length in *. - rewrite skipn_length in *. eapply Forall_app in H13. invs. + rewrite length_skipn in *. rewrite length_rev in *. + rewrite length_skipn in *. eapply Forall_app in H13. invs. eapply Forall_forall. intros. eapply Forall_forall in H12. 2: eassumption. @@ -5450,7 +5393,7 @@ Proof. eapply result_has_shape_result_shape_nat in H12, H13. rewrite H13 in H12. clear H13. pose proof Hsh. eapply result_has_shape_length in H13. - rewrite app_length in *. simpl length in *. rewrite repeat_length in *. + rewrite length_app in *. simpl length in *. rewrite repeat_length in *. subst. rewrite add_sub in *. rewrite minus_plus in *. @@ -5472,10 +5415,10 @@ Proof. rewrite rev_app_distr. repeat rewrite firstn_app. - rewrite rev_length. rewrite repeat_length. rewrite rev_repeat. + rewrite length_rev. rewrite repeat_length. rewrite rev_repeat. repeat rewrite skipn_app. rewrite repeat_length. rewrite add_sub. - repeat rewrite firstn_app. repeat rewrite skipn_length. + repeat rewrite firstn_app. repeat rewrite length_skipn. rewrite repeat_length. split. @@ -5586,7 +5529,7 @@ Proof. eapply result_has_shape_result_shape_nat in H12, H13. rewrite H13 in H12. clear H13. pose proof Hsh. eapply result_has_shape_length in H13. - rewrite app_length in *. simpl length in *. rewrite repeat_length in *. + rewrite length_app in *. simpl length in *. rewrite repeat_length in *. subst. rewrite add_sub in *. rewrite minus_plus in *. @@ -5607,11 +5550,11 @@ Proof. simpl in H13. invs. repeat rewrite firstn_app. repeat rewrite rev_app_distr. - repeat rewrite firstn_app. rewrite rev_repeat. rewrite rev_length. + repeat rewrite firstn_app. rewrite rev_repeat. rewrite length_rev. repeat rewrite skipn_app. repeat repeat rewrite firstn_app. - repeat rewrite rev_length. repeat rewrite skipn_length. + repeat rewrite length_rev. repeat rewrite length_skipn. rewrite repeat_length. - repeat rewrite add_sub. rewrite rev_length. + repeat rewrite add_sub. rewrite length_rev. replace (Z.to_nat (eval_Zexpr_Z_total $0 k) - (x + Z.to_nat (eval_Zexpr_Z_total $0 k))) with 0 by lia. rewrite sub_0_r. diff --git a/src/verified_lowering/proof/Range.v b/src/verified_lowering/proof/Range.v index e61c329..7f08742 100644 --- a/src/verified_lowering/proof/Range.v +++ b/src/verified_lowering/proof/Range.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Import ListNotations. Open Scope list_scope. @@ -178,7 +178,7 @@ Proof. 2: { erewrite length_concat. erewrite length_concat. rewrite repeat_length. - rewrite map_length. + rewrite length_map. rewrite length_zrange'. reflexivity. eapply Forall_repeat. reflexivity. eapply Forall_map. diff --git a/src/verified_lowering/proof/Result.v b/src/verified_lowering/proof/Result.v index 4062bc1..5125627 100644 --- a/src/verified_lowering/proof/Result.v +++ b/src/verified_lowering/proof/Result.v @@ -6,7 +6,7 @@ From Stdlib Require Import ZArith.Int. From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. Import ListNotations. @@ -289,7 +289,7 @@ Proof. - subst. econstructor. eauto. invert H0. eauto. invert H0. eauto. - subst. rewrite app_nil_r. econstructor. eauto. invert H. eauto. invert H. eauto. - - subst. econstructor. rewrite app_length. simpl. lia. + - subst. econstructor. rewrite length_app. simpl. lia. invert H. auto. eapply Forall_app. split; auto. invert H. auto. Qed. @@ -592,19 +592,19 @@ Proof. rewrite app_comm_cons. erewrite map_nat_range_extensionality. 2: { intros. rewrite skipn_app. rewrite firstn_app. - rewrite skipn_length. rewrite skipn_repeat. + rewrite length_skipn. rewrite skipn_repeat. rewrite firstn_repeat. simpl length. reflexivity. } eapply forall_result_has_shape. - 2: { rewrite map_length. unfold nat_range. + 2: { rewrite length_map. unfold nat_range. rewrite length_nat_range_rec. reflexivity. } eapply Forall_forall. intros. eapply in_map_iff in H0. invs. eapply In_nat_range in H2. eapply forall_result_has_shape. - 2: { rewrite app_length. rewrite firstn_length. - rewrite skipn_length. rewrite repeat_length. + 2: { rewrite length_app. rewrite length_firstn. + rewrite length_skipn. rewrite repeat_length. simpl length. cases (Datatypes.S (Datatypes.length l) mod k). - rewrite sub_0_r. rewrite Div0.mod_same by lia. rewrite sub_0_l. @@ -994,7 +994,7 @@ Proof. - invert H. simpl. eauto. - invert H0. rewrite app_nil_r. rewrite add_0_r. eauto. - simpl. invert H. invert H0. simpl. - econstructor. rewrite app_length. simpl. auto. auto. + econstructor. rewrite length_app. simpl. auto. auto. eapply Forall_app. auto. Qed. @@ -1045,7 +1045,7 @@ Proof. induct l1; intros. - subst. simpl in *. rewrite sub_0_r. auto. - simpl in *. invert H0. - rewrite app_length. + rewrite length_app. replace (Datatypes.S (Datatypes.length l1 + Datatypes.length l2) - Datatypes.S (Datatypes.length l1)) with (length l2) by lia. eapply Forall_app in H7. invs. @@ -1061,7 +1061,7 @@ Proof. - subst. simpl in *. erewrite result_has_shape_length by eauto. rewrite sub_diag. econstructor. - simpl in *. invert H0. - rewrite app_length. + rewrite length_app. replace (Datatypes.S (Datatypes.length l1 + Datatypes.length l2) - (Datatypes.length l2)) with (Datatypes.S (length l1)) by lia. eapply Forall_app in H7. invs. @@ -1132,7 +1132,7 @@ Proof. 2 : { discriminate. } pose proof Heq. eapply nth_error_Some in Heq. - rewrite app_length in *. + rewrite length_app in *. rewrite repeat_length in *. assert (Z.pos p < Z.of_nat (length x) \/ Z.pos p >= Z.of_nat (length x))%Z by lia. @@ -1701,7 +1701,7 @@ Proof. - invert H. cases a. invert H6. simpl. rewrite rev_app_distr. rewrite firstn_app. pose proof H6. eapply result_has_shape_length in H. - repeat rewrite rev_length. + repeat rewrite length_rev. erewrite result_has_shape_length. 2: { eapply result_has_shape_flatten. eapply forall_result_has_shape. eauto. reflexivity. } @@ -1714,8 +1714,8 @@ Proof. cases (k - length l). * simpl. econstructor. * simpl. rewrite firstn_all2. - 2: { rewrite rev_length. eapply Nat.le_add_r. } - rewrite rev_length in *. rewrite Heq in *. simpl in *. invert H2. + 2: { rewrite length_rev. eapply Nat.le_add_r. } + rewrite length_rev in *. rewrite Heq in *. simpl in *. invert H2. invert H3. rewrite rev_repeat. eapply Forall_repeat. eauto. Qed. @@ -1828,7 +1828,7 @@ Proof. 2: lia. rewrite firstn_all2. reflexivity. - rewrite rev_length. + rewrite length_rev. erewrite result_has_shape_length. 2: { eapply result_has_shape_transpose_result_list. 2: econstructor; eauto. lia. } @@ -1841,7 +1841,7 @@ Proof. reflexivity. 2: econstructor; eauto. lia. } rewrite <- (rev_involutive (transpose_result_list _ _)). rewrite skipn_rev. - rewrite rev_involutive. rewrite rev_length. rewrite H. + rewrite rev_involutive. rewrite length_rev. rewrite H. erewrite IHm0. 2: econstructor; eauto. 2: lia. @@ -1886,8 +1886,8 @@ Proof. + simpl in *. eapply forall_eq_gen_pad in H4. simpl in *. rewrite firstn_all2 in H4. - 2: { rewrite rev_length. lia. } - rewrite rev_length in *. + 2: { rewrite length_rev. lia. } + rewrite length_rev in *. rewrite <- rev_repeat in H4. assert (rev (rev v) = rev (rev (repeat (gen_pad sh) (Datatypes.length v)))). @@ -1902,8 +1902,8 @@ Proof. rewrite repeat_length in *. lia. eapply nth_error_None in Heq0. lia. + rewrite nth_error_app2. - 2: { rewrite firstn_length. lia. } - rewrite firstn_length. rewrite H3. + 2: { rewrite length_firstn. lia. } + rewrite length_firstn. rewrite H3. replace (min (Datatypes.S n0) m) with (Datatypes.S n0) by lia. eapply forall_eq_gen_pad in H4. rewrite firstn_rev in H4. @@ -1911,7 +1911,7 @@ Proof. rewrite <- Heq. rewrite H3 in *. rewrite H4. simpl gen_pad_list. rewrite rev_repeat. - rewrite rev_length. rewrite skipn_length. + rewrite length_rev. rewrite length_skipn. rewrite H3. replace (m - (m-n)) with n by lia. rewrite nth_error_repeat. @@ -1950,8 +1950,8 @@ Proof. simpl in Heq. rewrite map_cons. simpl. cases (nth_error (rev v ++ [r]) i). - 2: { eapply nth_error_None in Heq0. rewrite app_length in *. - rewrite rev_length in *. simpl in *. + 2: { eapply nth_error_None in Heq0. rewrite length_app in *. + rewrite length_rev in *. simpl in *. pose proof H6. eapply result_has_shape_length in H1. simpl in H1. subst. lia. } f_equal. @@ -1963,8 +1963,8 @@ Proof. pose proof H6. eapply result_has_shape_length in H. subst. simpl in *. rewrite sub_0_r in *. rewrite nth_error_app2. - 2: { rewrite rev_length. lia. } - rewrite rev_length. + 2: { rewrite length_rev. lia. } + rewrite length_rev. erewrite <- IHl. 2: eapply forall_result_has_shape; eauto. 2: lia. @@ -2005,7 +2005,7 @@ Proof. erewrite get_col_empty. reflexivity. eapply forall_result_has_shape. eapply forall_firstn. - econstructor; eauto. rewrite firstn_length. + econstructor; eauto. rewrite length_firstn. simpl. reflexivity. eapply result_has_shape_length in H5. lia. Qed. @@ -2047,7 +2047,7 @@ Proof. erewrite get_col_empty. reflexivity. eapply forall_result_has_shape. eapply forall_skipn. - econstructor; eauto. rewrite skipn_length. + econstructor; eauto. rewrite length_skipn. simpl. reflexivity. eapply result_has_shape_length in H5. lia. Qed. @@ -2071,10 +2071,10 @@ Proof. eapply result_has_shape_length in H3. rewrite <- (firstn_skipn n v). rewrite nth_error_app1. - 2: { rewrite firstn_length. lia. } + 2: { rewrite length_firstn. lia. } eapply forall_eq_gen_pad in H4. rewrite H4. simpl. rewrite nth_error_repeat. - 2: { rewrite firstn_length. lia. } + 2: { rewrite length_firstn. lia. } f_equal. erewrite IHl. reflexivity. eauto. 2: eapply forall_result_has_shape; eauto. @@ -2104,10 +2104,10 @@ Proof. - simpl. eauto. - simpl. invert H. cases a. - + econstructor. rewrite map_length. reflexivity. eauto. + + econstructor. rewrite length_map. reflexivity. eauto. eapply result_has_shape_forall. eapply IHl. eapply forall_result_has_shape. eauto. reflexivity. - + econstructor. rewrite map_length. reflexivity. + + econstructor. rewrite length_map. reflexivity. eapply result_has_shape_rev. eauto. eapply result_has_shape_forall. eapply IHl. eapply forall_result_has_shape. eauto. reflexivity. @@ -2230,7 +2230,7 @@ Proof. invert H0. lia. auto. } 2: { invert H7. lia. econstructor. eauto. eauto. } rewrite rev_app_distr. rewrite firstn_app. - erewrite rev_length. erewrite result_has_shape_length. + erewrite length_rev. erewrite result_has_shape_length. 2: { simpl. cases a. invert H7. rewrite app_nil_r. eauto. } simpl. cases a. invert H7. rewrite app_nil_r. rewrite Forall_app. invert H. split. eauto. @@ -2262,7 +2262,7 @@ Proof. simpl. intros. invert H0. lia. eauto. } 2: { econstructor. invert H8. lia. eauto. eauto. } rewrite rev_app_distr. rewrite skipn_app. rewrite firstn_app. - rewrite skipn_length. repeat rewrite rev_length. + rewrite length_skipn. repeat rewrite length_rev. simpl length. cases a. invert H8. simpl. rewrite app_nil_r. erewrite result_has_shape_length by eauto. pose proof (Nat.sub_0_le b m). inversion H0. erewrite H4 by lia. @@ -2288,7 +2288,7 @@ Proof. - simpl in *. invert H0. cases a. invert H8. invert H. rewrite skipn_app. rewrite firstn_app. rewrite Forall_app. split. auto. - rewrite skipn_length. erewrite result_has_shape_length by eauto. + rewrite length_skipn. erewrite result_has_shape_length by eauto. pose proof (Nat.sub_0_le a0 m). inversion H. erewrite H3 by lia. replace (l1 - (m - a0)) with 0 by lia. econstructor. @@ -2356,9 +2356,9 @@ Proof. rewrite min_0_r. simpl repeat at 1. rewrite app_nil_r. f_equal. erewrite <- IHn with (sh:=sh) (c:=c+1). - rewrite skipn_length. simpl length. + rewrite length_skipn. simpl length. 2: lia. - 2: { simpl in *. rewrite skipn_length. simpl length in *. lia. } + 2: { simpl in *. rewrite length_skipn. simpl length in *. lia. } 2: { eapply forall_result_has_shape. eapply forall_skipn. invert H1. econstructor. eauto. eauto. reflexivity. } f_equal. eapply map_nat_range_rec_extensionality. @@ -2460,7 +2460,7 @@ Proof. assert (n0 = (length (r::l)) / k) by lia. subst. rewrite app_comm_cons. rewrite skipn_app. rewrite firstn_app. rewrite skipn_repeat. rewrite firstn_repeat. - rewrite skipn_length. repeat rewrite app_assoc. f_equal. + rewrite length_skipn. repeat rewrite app_assoc. f_equal. 2: { f_equal. simpl length in *. replace (k * (Datatypes.S (length l) / k) - Datatypes.S (length l)) with 0. @@ -2491,7 +2491,7 @@ Proof. erewrite map_nat_range_rec_extensionality. 2: { intros. rewrite skipn_app. rewrite firstn_app. rewrite skipn_repeat. rewrite firstn_repeat. - rewrite skipn_length. + rewrite length_skipn. rewrite (Nat.div_mod_eq (Datatypes.length (r::l)) k) at 2. rewrite sub_add_distr. rewrite <- mul_sub_distr_l. @@ -2509,7 +2509,7 @@ Proof. rewrite H2. 2: lia. 2: { pose proof (Div0.mul_div_le (length (r::l)) k). lia. } rewrite firstn_all2 with (n:=k). - 2: { rewrite skipn_length. rewrite <- Div0.mod_eq by lia. + 2: { rewrite length_skipn. rewrite <- Div0.mod_eq by lia. pose proof (Nat.mod_upper_bound (length (r::l)) k). lia. } symmetry. rewrite <- firstn_skipn with (n:=(Datatypes.length (r :: l) / k * k)) @@ -2614,7 +2614,7 @@ Proof. rewrite app_comm_cons. rewrite skipn_app. simpl length. rewrite nth_error_app1. - 2: { rewrite skipn_length. simpl length in *. + 2: { rewrite length_skipn. simpl length in *. eapply Nat.add_lt_mono_l with (p:=k * (x / k)). rewrite <- div_mod by lia. rewrite Nat.add_comm. diff --git a/src/verified_lowering/proof/ResultToArrayDelta.v b/src/verified_lowering/proof/ResultToArrayDelta.v index a9dfad2..1b78216 100644 --- a/src/verified_lowering/proof/ResultToArrayDelta.v +++ b/src/verified_lowering/proof/ResultToArrayDelta.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. @@ -895,7 +895,7 @@ Proof. posnats. unfold shape_to_vars. simpl. rewrite shape_to_index_cons. rewrite index_to_partial_function_vars_cons by eauto with reindexers. - unfold nat_range. repeat rewrite map_length. + unfold nat_range. repeat rewrite length_map. rewrite Hmap by (eapply not_var_generation_in_index; eauto). rewrite map_cons. unfold subst_var_in_Z_tup at 1. simpl. posnats. @@ -917,15 +917,15 @@ Proof. rewrite fold_left_subst_var_in_Z_tup_ZLit. rewrite map_fold_left_subst_var_in_Z_tup_shape_to_index. reflexivity. - rewrite map_length. rewrite length_nat_range_rec. + rewrite length_map. rewrite length_nat_range_rec. eapply length_mesh_grid_indices. decomp_index. auto. eapply no_dup_var_generation. - rewrite map_length. rewrite length_nat_range_rec. + rewrite length_map. rewrite length_nat_range_rec. eapply length_mesh_grid_indices. decomp_index. auto. eapply no_dup_var_generation. - rewrite map_length. rewrite length_nat_range_rec. + rewrite length_map. rewrite length_nat_range_rec. eapply length_mesh_grid_indices. decomp_index. auto. - rewrite map_length. rewrite length_nat_range_rec. + rewrite length_map. rewrite length_nat_range_rec. eapply length_mesh_grid_indices. decomp_index. auto. eapply not_In_var_map. lia. eapply partial_injective_cons_0. apply Hinj. diff --git a/src/verified_lowering/proof/Sexpr.v b/src/verified_lowering/proof/Sexpr.v index 115a3ec..944ec51 100644 --- a/src/verified_lowering/proof/Sexpr.v +++ b/src/verified_lowering/proof/Sexpr.v @@ -8,7 +8,7 @@ From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. From Stdlib Require Import Reals.Rpower. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. From Stdlib Require Import Reals.Reals. Import Rdefinitions. Import RIneq. Set Warnings "-deprecate-hint-without-locality,-deprecated". diff --git a/src/verified_lowering/proof/VarGeneration.v b/src/verified_lowering/proof/VarGeneration.v index f694b5e..838e8e4 100644 --- a/src/verified_lowering/proof/VarGeneration.v +++ b/src/verified_lowering/proof/VarGeneration.v @@ -1,7 +1,7 @@ From Stdlib Require Import ZArith.Zdiv. From Stdlib Require Import ZArith.Int. From Stdlib Require Import ZArith.Znat. -Require Import String. +From Stdlib Require Import String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. diff --git a/src/verified_lowering/proof/WellFormedAllocation.v b/src/verified_lowering/proof/WellFormedAllocation.v index 60a0e43..ffa80a2 100644 --- a/src/verified_lowering/proof/WellFormedAllocation.v +++ b/src/verified_lowering/proof/WellFormedAllocation.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. @@ -979,17 +979,17 @@ Proof. eapply eq_zexpr_mul_literal. eapply eq_zexpr_id. f_equal. lia. eapply eq_Z_tuple_index_list_id. - rewrite map_length. rewrite length_nat_range_rec. - rewrite map_length. eapply length_mesh_grid_indices. + rewrite length_map. rewrite length_nat_range_rec. + rewrite length_map. eapply length_mesh_grid_indices. erewrite <- in_mesh_grid_cons_filter_until_0. auto. - rewrite map_length. rewrite length_nat_range_rec. - rewrite map_length. eapply length_mesh_grid_indices. + rewrite length_map. rewrite length_nat_range_rec. + rewrite length_map. eapply length_mesh_grid_indices. erewrite <- in_mesh_grid_cons_filter_until_0. auto. assert (-1 * z1 <= z0* Z.of_nat (Datatypes.S m))%Z by lia. assert (-1 * Z.of_nat (Datatypes.S m) < -1 * z1)%Z by lia. assert (-1 * Z.of_nat (Datatypes.S m) < z0* Z.of_nat (Datatypes.S m))%Z by lia. - eapply Zmult_gt_0_lt_reg_r in H12. + eapply Zorder.Zmult_gt_0_lt_reg_r in H12. erewrite <- in_mesh_grid_cons_filter_until_0. simpl map. erewrite <- in_mesh_grid_cons__. propositional. lia. @@ -1050,11 +1050,11 @@ Proof. eapply eq_zexpr_mul_literal. eapply eq_zexpr_id. f_equal. lia. eapply eq_Z_tuple_index_list_id. - rewrite map_length. rewrite length_nat_range_rec. - rewrite map_length. eapply length_mesh_grid_indices. + rewrite length_map. rewrite length_nat_range_rec. + rewrite length_map. eapply length_mesh_grid_indices. erewrite <- in_mesh_grid_cons_filter_until_0. auto. - rewrite map_length. rewrite length_nat_range_rec. - rewrite map_length. eapply length_mesh_grid_indices. + rewrite length_map. rewrite length_nat_range_rec. + rewrite length_map. eapply length_mesh_grid_indices. erewrite <- in_mesh_grid_cons_filter_until_0. auto. simpl map. cases n. simpl in *. lia. simpl map. posnats. @@ -2462,4 +2462,3 @@ Proof. eauto. lia. eassumption. lia. rewrite Z2Nat.id by lia. eauto. eauto. eauto. eauto. eauto. eauto. eauto. lia. lia. eauto. lia. Qed. - diff --git a/src/verified_lowering/proof/WellFormedEnvironment.v b/src/verified_lowering/proof/WellFormedEnvironment.v index bea78c5..f763bec 100644 --- a/src/verified_lowering/proof/WellFormedEnvironment.v +++ b/src/verified_lowering/proof/WellFormedEnvironment.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. diff --git a/src/verified_lowering/proof/WellFormedReindexer.v b/src/verified_lowering/proof/WellFormedReindexer.v index 70b4eeb..c541c3f 100644 --- a/src/verified_lowering/proof/WellFormedReindexer.v +++ b/src/verified_lowering/proof/WellFormedReindexer.v @@ -9,7 +9,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Strings.String. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. @@ -1161,7 +1161,7 @@ Proof. assert (-1 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)) < z0 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)))%Z by lia. - eapply Zmult_lt_reg_r in H11. + eapply Zorder.Zmult_lt_reg_r in H11. lia. lia. rewrite Nat2Z.inj_mul in H10. rewrite @@ -1171,7 +1171,7 @@ Proof. assert (-1 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)) < z0 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)))%Z by lia. - eapply Zmult_lt_reg_r in H11. + eapply Zorder.Zmult_lt_reg_r in H11. lia. lia. lia. repeat decomp_goal_index. propositional. @@ -1181,7 +1181,7 @@ Proof. assert (-1 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)) < z0 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)))%Z by lia. - eapply Zmult_lt_reg_r in H11. + eapply Zorder.Zmult_lt_reg_r in H11. lia. lia. rewrite Nat2Z.inj_mul in H10. rewrite @@ -1191,7 +1191,7 @@ Proof. assert (-1 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)) < z0 * Z.of_nat (Z.to_nat (eval_Zexpr_Z_total $0 m)))%Z by lia. - eapply Zmult_lt_reg_r in H11. + eapply Zorder.Zmult_lt_reg_r in H11. lia. lia. eauto. eauto. lia. lia. diff --git a/src/verified_lowering/proof/Zexpr.v b/src/verified_lowering/proof/Zexpr.v index 4eb4114..c0d287d 100644 --- a/src/verified_lowering/proof/Zexpr.v +++ b/src/verified_lowering/proof/Zexpr.v @@ -7,7 +7,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Lists.List. From Stdlib Require Import micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.FunctionalExtensionality. Set Warnings "-deprecate-hint-without-locality,-deprecated". Import ListNotations. diff --git a/src/verified_scheduling/atl/.Makefile.coq.d b/src/verified_scheduling/atl/.Makefile.coq.d deleted file mode 100644 index c60124a..0000000 --- a/src/verified_scheduling/atl/.Makefile.coq.d +++ /dev/null @@ -1,48 +0,0 @@ -ATL.vo ATL.glob ATL.v.beautified ATL.required_vo: ATL.v -ATL.vio: ATL.v -ATL.vos ATL.vok ATL.required_vos: ATL.v -Tactics.vo Tactics.glob Tactics.v.beautified Tactics.required_vo: Tactics.v ATL.vo -Tactics.vio: Tactics.v ATL.vio -Tactics.vos Tactics.vok Tactics.required_vos: Tactics.v ATL.vos -Relations.vo Relations.glob Relations.v.beautified Relations.required_vo: Relations.v -Relations.vio: Relations.v -Relations.vos Relations.vok Relations.required_vos: Relations.v -Invariant.vo Invariant.glob Invariant.v.beautified Invariant.required_vo: Invariant.v Relations.vo -Invariant.vio: Invariant.v Relations.vio -Invariant.vos Invariant.vok Invariant.required_vos: Invariant.v Relations.vos -Sets.vo Sets.glob Sets.v.beautified Sets.required_vo: Sets.v -Sets.vio: Sets.v -Sets.vos Sets.vok Sets.required_vos: Sets.v -ModelCheck.vo ModelCheck.glob ModelCheck.v.beautified ModelCheck.required_vo: ModelCheck.v Invariant.vo Relations.vo Sets.vo -ModelCheck.vio: ModelCheck.v Invariant.vio Relations.vio Sets.vio -ModelCheck.vos ModelCheck.vok ModelCheck.required_vos: ModelCheck.v Invariant.vos Relations.vos Sets.vos -Var.vo Var.glob Var.v.beautified Var.required_vo: Var.v -Var.vio: Var.v -Var.vos Var.vok Var.required_vos: Var.v -Map.vo Map.glob Map.v.beautified Map.required_vo: Map.v Sets.vo -Map.vio: Map.v Sets.vio -Map.vos Map.vok Map.required_vos: Map.v Sets.vos -FrapWithoutSets.vo FrapWithoutSets.glob FrapWithoutSets.v.beautified FrapWithoutSets.required_vo: FrapWithoutSets.v Sets.vo Map.vo Var.vo Invariant.vo ModelCheck.vo Relations.vo -FrapWithoutSets.vio: FrapWithoutSets.v Sets.vio Map.vio Var.vio Invariant.vio ModelCheck.vio Relations.vio -FrapWithoutSets.vos FrapWithoutSets.vok FrapWithoutSets.required_vos: FrapWithoutSets.v Sets.vos Map.vos Var.vos Invariant.vos ModelCheck.vos Relations.vos -Div.vo Div.glob Div.v.beautified Div.required_vo: Div.v Tactics.vo FrapWithoutSets.vo -Div.vio: Div.v Tactics.vio FrapWithoutSets.vio -Div.vos Div.vok Div.required_vos: Div.v Tactics.vos FrapWithoutSets.vos -Common.vo Common.glob Common.v.beautified Common.required_vo: Common.v ATL.vo Tactics.vo Div.vo -Common.vio: Common.v ATL.vio Tactics.vio Div.vio -Common.vos Common.vok Common.required_vos: Common.v ATL.vos Tactics.vos Div.vos -CommonTactics.vo CommonTactics.glob CommonTactics.v.beautified CommonTactics.required_vo: CommonTactics.v ATL.vo Tactics.vo Div.vo Common.vo -CommonTactics.vio: CommonTactics.v ATL.vio Tactics.vio Div.vio Common.vio -CommonTactics.vos CommonTactics.vok CommonTactics.required_vos: CommonTactics.v ATL.vos Tactics.vos Div.vos Common.vos -LetLifting.vo LetLifting.glob LetLifting.v.beautified LetLifting.required_vo: LetLifting.v ATL.vo Common.vo Tactics.vo CommonTactics.vo -LetLifting.vio: LetLifting.v ATL.vio Common.vio Tactics.vio CommonTactics.vio -LetLifting.vos LetLifting.vok LetLifting.required_vos: LetLifting.v ATL.vos Common.vos Tactics.vos CommonTactics.vos -GenPushout.vo GenPushout.glob GenPushout.v.beautified GenPushout.required_vo: GenPushout.v ATL.vo Common.vo Tactics.vo Div.vo CommonTactics.vo -GenPushout.vio: GenPushout.v ATL.vio Common.vio Tactics.vio Div.vio CommonTactics.vio -GenPushout.vos GenPushout.vok GenPushout.required_vos: GenPushout.v ATL.vos Common.vos Tactics.vos Div.vos CommonTactics.vos -Reshape.vo Reshape.glob Reshape.v.beautified Reshape.required_vo: Reshape.v ATL.vo Tactics.vo Common.vo CommonTactics.vo Div.vo GenPushout.vo LetLifting.vo -Reshape.vio: Reshape.v ATL.vio Tactics.vio Common.vio CommonTactics.vio Div.vio GenPushout.vio LetLifting.vio -Reshape.vos Reshape.vok Reshape.required_vos: Reshape.v ATL.vos Tactics.vos Common.vos CommonTactics.vos Div.vos GenPushout.vos LetLifting.vos -PairElimination.vo PairElimination.glob PairElimination.v.beautified PairElimination.required_vo: PairElimination.v ATL.vo Common.vo CommonTactics.vo Tactics.vo Div.vo -PairElimination.vio: PairElimination.v ATL.vio Common.vio CommonTactics.vio Tactics.vio Div.vio -PairElimination.vos PairElimination.vok PairElimination.required_vos: PairElimination.v ATL.vos Common.vos CommonTactics.vos Tactics.vos Div.vos diff --git a/src/verified_scheduling/atl/ATL.v b/src/verified_scheduling/atl/ATL.v index 5f6d793..4ca3c6c 100644 --- a/src/verified_scheduling/atl/ATL.v +++ b/src/verified_scheduling/atl/ATL.v @@ -7,6 +7,7 @@ From Stdlib Require Import Reals.Reals. Import RIneq. Import Rdefinitions. From Stdlib Require Import ZArith.Int. From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Logic.FunctionalExtensionality. +Import BinNatDef. Import ListNotations. @@ -405,9 +406,8 @@ Proof. - simpl. destruct i; try reflexivity. simpl. rewrite Z.add_0_r. reflexivity. - apply lt_S_n in H0. - apply (IHn _ m ((fun x => e0 (x+1)%Z))) in H0. simpl. - rewrite H0. rewrite <- Z.add_assoc. + specialize (IHn i m (fun x => e0 (x+1)%Z) ltac:(lia)). + simpl. rewrite IHn. rewrite <- Z.add_assoc. rewrite Zpos_P_of_succ_nat. reflexivity. Qed. @@ -555,7 +555,7 @@ Proof. apply IHn. eapply tensor_consistent_step. eauto. eapply tensor_consistent_step. eauto. - rewrite map_length. simpl in *. lia. + rewrite length_map. simpl in *. lia. } { @@ -637,7 +637,7 @@ Proof. simpl. constructor. auto. auto. simpl in *. - rewrite map_length in *. lia. + rewrite length_map in *. lia. } { @@ -706,18 +706,18 @@ Proof. rewrite tensor_add_empty_r. f_equal. - simpl. unfold tensor_add. - simpl length. rewrite map_length. + simpl length. rewrite length_map. unfold gen, genr. erewrite map_gen_helper. repeat rewrite Z.sub_0_r. repeat rewrite Nat2Z.id. simpl. erewrite mul_bin_distr. - f_equal. rewrite map_length. + f_equal. rewrite length_map. eapply gen_helper_eq_bound. intros. rewrite Z.add_0_r. rewrite mul_bin_distr. repeat rewrite <- map_cons. assert (i < length a0 \/ length a0 <= i) by lia. inversion H2; clear H2. + erewrite get_cons by lia. simpl. erewrite (get_cons _ (map _ a0)). - 2: lia. 2: rewrite map_length; lia. f_equal. + 2: lia. 2: rewrite length_map; lia. f_equal. * unfold get. destruct a0. -- simpl in *. lia. @@ -738,11 +738,11 @@ Proof. + erewrite get_znlt_null by (simpl in *; lia). simpl. symmetry. erewrite get_znlt_null. - 2: { simpl. rewrite map_length. lia. } + 2: { simpl. rewrite length_map. lia. } unfold iverson. f_equal. eapply scalar_mul_comm. erewrite get_cons. 2: lia. - 2: { rewrite map_length. lia. } + 2: { rewrite length_map. lia. } erewrite get_cons by lia. unfold get. destruct b. @@ -776,7 +776,7 @@ Proof. intros. induction e. - simpl. reflexivity. - - unfold tensor_add. rewrite map_length. + - unfold tensor_add. rewrite length_map. rewrite max_id. symmetry. erewrite <- (get_gen_id (a::e)) at 1. 2: reflexivity. eapply gen_eq_bound; intros. diff --git a/src/verified_scheduling/atl/Common.v b/src/verified_scheduling/atl/Common.v index 721d307..f26e7a4 100644 --- a/src/verified_scheduling/atl/Common.v +++ b/src/verified_scheduling/atl/Common.v @@ -12,6 +12,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Setoids.Setoid. From Stdlib Require Import Logic.FunctionalExtensionality. From Stdlib Require Import Classes.Morphisms. +Import Zorder. Set Warnings "-deprecate-hint-without-locality,-deprecated". @@ -39,9 +40,7 @@ Lemma nth_map {X} `{TensorElem X} : forall i f v, Proof. induction i; intros f v H0; destruct v; simpl in *; try contra_crush; auto. - apply lt_S_n in H0. - eapply IHi in H0. - apply H0. + apply IHi. lia. Qed. (* Hole Establishing and Context Diving *) @@ -494,11 +493,8 @@ Proof. - simpl. destruct i; try reflexivity. simpl. rewrite Z.add_0_r. reflexivity. - apply lt_S_n in H0. - apply (IHn _ m (inc e0)) in H0. simpl. - rewrite H0. rewrite <- Z.add_assoc. - rewrite Zpos_P_of_succ_nat. - reflexivity. + simpl. rewrite IHn by lia. + f_equal. f_equal. lia. Qed. Lemma get_gen_helper_some {X} `{TensorElem X} : forall n m f i, @@ -734,7 +730,7 @@ Lemma iverson_length {X} `{TensorElem X} : forall b (l : list X), length (|[ b ]| l) = length l. Proof. destruct b; intros; simpl; unfold iverson; unfold scalar_mul; simpl; - rewrite map_length; auto. + rewrite length_map; auto. Qed. Hint Rewrite @iverson_length : crunch. @@ -1891,8 +1887,7 @@ Lemma gen_neg_empty {X} `{TensorElem X} : forall n f, Proof. intros. destruct n. - lia. - - specialize (Zgt_pos_0 p). intros. - lia. + - lia. - reflexivity. Qed. @@ -2489,7 +2484,7 @@ Proof. pose proof (Z.mod_pos_bound i (Z.of_nat k)). peel_hyp. auto with crunch. - destruct (0 <=? i/zk - i1)%Z eqn:e; unbool_hyp. + auto. - + assert ((i / zk - i1) * zk <= - zk)%Z . + + assert ((i / zk - i1) * zk <= - zk)%Z. apply Zle_0_minus_le. replace (-zk)%Z with ((-1)*zk)%Z by lia. rewrite <- Z.mul_sub_distr_r. @@ -2749,7 +2744,7 @@ Proof. reflexivity. assert (length (scalar_mul 0 x :: List.map (scalar_mul 0) e) <= Pos.to_nat p). - { simpl. rewrite map_length. simpl in *. zify. lia. } + { simpl. rewrite length_map. simpl in *. zify. lia. } zify. lia. - zify. lia. Qed. diff --git a/src/verified_scheduling/atl/CommonTactics.v b/src/verified_scheduling/atl/CommonTactics.v index 7d03a95..f437f89 100644 --- a/src/verified_scheduling/atl/CommonTactics.v +++ b/src/verified_scheduling/atl/CommonTactics.v @@ -86,7 +86,7 @@ Ltac ttt e := (assert (0 <= I)%Z as t by (auto + lia); clear t) | (destruct (0 <=? I)%Z eqn:t; - [ apply Zle_bool_imp_le in t | apply Z.leb_gt in t]) + [ apply Zbool.Zle_bool_imp_le in t | apply Z.leb_gt in t]) ]; first [ (assert (I < V)%Z as t' by (auto + lia); clear t') @@ -100,7 +100,7 @@ Ltac ttt e := (assert (0 <= I)%Z as t by (auto + lia); clear t) | (destruct (0 <=? I)%Z eqn:t; - [ apply Zle_bool_imp_le in t | apply Z.leb_gt in t]) + [ apply Zbool.Zle_bool_imp_le in t | apply Z.leb_gt in t]) ]; first [ (assert (I < Z.of_nat (length V))%Z as t' by (auto + lia); clear t') diff --git a/src/verified_scheduling/atl/Div.v b/src/verified_scheduling/atl/Div.v index ef72926..e491a64 100644 --- a/src/verified_scheduling/atl/Div.v +++ b/src/verified_scheduling/atl/Div.v @@ -11,6 +11,7 @@ From Stdlib Require Import ZArith.Znat. From Stdlib Require Import Setoids.Setoid. From Stdlib Require Import Logic.FunctionalExtensionality. From Stdlib Require Import Classes.Morphisms. +Import Zorder. From ATL Require Import Tactics FrapWithoutSets. @@ -71,14 +72,8 @@ Proof. { apply Z.mul_le_mono_nonneg_r. lia. lia. } - assert ((n-1)*m + j < (n-1)*m + m). - { - apply Zplus_lt_compat_l. auto. - } - assert (i*m + j <= (n-1)*m + j). - { - apply Zplus_le_compat_r. auto. - } + assert ((n-1)*m + j < (n-1)*m + m) by lia. + assert (i*m + j <= (n-1)*m + j) by lia. eapply Z.le_lt_trans. apply H5. rewrite Zmult_succ_l_reverse in H4. @@ -180,8 +175,7 @@ Proof. - simpl in *. lia. - rewrite <- e in *. apply Z2Nat.inj_lt in H; auto. - subst. - apply Zle_0_pos. + subst. lia. - simpl in *. lia. Qed. @@ -332,9 +326,9 @@ Hint Resolve Z.div_pos : crunch. Lemma expand_Zmod : forall i m, (0 < m)%Z -> - (i - i / m * m = Coq.ZArith.BinIntDef.Z.modulo i m)%Z. + (i - i / m * m = Stdlib.ZArith.BinIntDef.Z.modulo i m)%Z. Proof. - intros. unfold Coq.ZArith.BinIntDef.Z.modulo. + intros. unfold Stdlib.ZArith.BinIntDef.Z.modulo. pose proof (Z_div_mod i m). assert (m > 0)%Z by lia. apply H0 in H1. diff --git a/src/verified_scheduling/atl/FrapWithoutSets.v b/src/verified_scheduling/atl/FrapWithoutSets.v index cd2cbcb..54e933c 100644 --- a/src/verified_scheduling/atl/FrapWithoutSets.v +++ b/src/verified_scheduling/atl/FrapWithoutSets.v @@ -1,7 +1,7 @@ From ATL Require Import Sets Map Var Invariant ModelCheck. -Require Import Eqdep String NArith Arith Lia Program Relations Bool. +From Stdlib Require Import Eqdep String NArith Arith Lia Program Relations Bool. Export Ascii String Arith Sets Relations Map Var Invariant Bool ModelCheck. -Require Import List. +From Stdlib Require Import List. Export List ListNotations. Open Scope string_scope. Open Scope list_scope. @@ -389,7 +389,7 @@ Ltac simplify_map := replace (@add A B m k v) with m' by maps_equal) end. -Require Import Classical. +From Stdlib Require Import Classical. Ltac excluded_middle P := destruct (classic P). Lemma join_idempotent: forall (A B : Type) (m : fmap A B), (m $++ m) = m. diff --git a/src/verified_scheduling/atl/Map.v b/src/verified_scheduling/atl/Map.v index 389fd6d..115fe5a 100644 --- a/src/verified_scheduling/atl/Map.v +++ b/src/verified_scheduling/atl/Map.v @@ -1,4 +1,4 @@ -Require Import Classical ClassicalEpsilon FunctionalExtensionality. +From Stdlib Require Import Classical ClassicalEpsilon FunctionalExtensionality. From ATL Require Import Sets. Set Implicit Arguments. diff --git a/src/verified_scheduling/atl/ModelCheck.v b/src/verified_scheduling/atl/ModelCheck.v index 594894b..e4a9dce 100644 --- a/src/verified_scheduling/atl/ModelCheck.v +++ b/src/verified_scheduling/atl/ModelCheck.v @@ -1,4 +1,5 @@ -Require Import Invariant Relations Sets Classical. +From Stdlib Require Import Classical. +Require Import Sets Invariant Relations. Set Implicit Arguments. diff --git a/src/verified_scheduling/atl/Reshape.v b/src/verified_scheduling/atl/Reshape.v index 6d637c9..204528a 100644 --- a/src/verified_scheduling/atl/Reshape.v +++ b/src/verified_scheduling/atl/Reshape.v @@ -13,6 +13,7 @@ From Stdlib Require Import Setoids.Setoid. From Stdlib Require Import Logic.FunctionalExtensionality. From Stdlib Require Import Classes.Morphisms. Import ListNotations. +Import Zorder. From ATL Require Import ATL Tactics Common CommonTactics Div GenPushout LetLifting. diff --git a/src/verified_scheduling/atl/Sets.v b/src/verified_scheduling/atl/Sets.v index 88ff7b4..0f299f8 100644 --- a/src/verified_scheduling/atl/Sets.v +++ b/src/verified_scheduling/atl/Sets.v @@ -1,4 +1,4 @@ -Require Import Bool Classical FunctionalExtensionality List. +From Stdlib Require Import Bool Classical FunctionalExtensionality List. Set Implicit Arguments. @@ -288,7 +288,7 @@ Ltac unifyTails := (** * But wait... there's a reflective way to do some of this, too. *) -Require Import Arith. +From Stdlib Require Import Arith. Import List ListNotations. Section setexpr. diff --git a/src/verified_scheduling/atl/Tactics.v b/src/verified_scheduling/atl/Tactics.v index 4c25ba2..dca4f09 100644 --- a/src/verified_scheduling/atl/Tactics.v +++ b/src/verified_scheduling/atl/Tactics.v @@ -52,7 +52,7 @@ Ltac unbool_hyp := | [ H : (false = _) |- _ ] => symmetry in H | [ H : (_ =? _ = true) |- _ ] => apply eqb_eq in H | [ H : (_ =? _ = false) |- _ ] => apply eqb_neq in H - | [ H : (_ <=? _ = true) |- _ ] => apply Zle_is_le_bool in H + | [ H : (_ <=? _ = true) |- _ ] => apply Zbool.Zle_bool_imp_le in H | [ H : (_ <=? _ = false) |- _ ] => apply leb_gt in H | [ H : (_ apply ltb_lt in H | [ H : (_ apply ltb_ge in H @@ -99,7 +99,7 @@ Ltac contra_crush := try (simpl in *; | [ H : ~ ?A |- _] => (assert A by (try assumption; try lia; try ring)); contradiction | [ H : 0 <= Z.neg ?A |- _ ] => - specialize (Zlt_neg_0 A); intros; contradiction + specialize (Zorder.Zlt_neg_0 A); intros; contradiction | [ H : 0 < Z.neg _ |- _ ] => now inversion H | [ H : Z.pos _ < Z.neg _ |- _ ] => now inversion H end). diff --git a/src/verified_scheduling/atl/Var.v b/src/verified_scheduling/atl/Var.v index a007ff5..a97482f 100644 --- a/src/verified_scheduling/atl/Var.v +++ b/src/verified_scheduling/atl/Var.v @@ -1,5 +1,4 @@ -Require Import String. -From Stdlib Require Import Lists.List. +From Stdlib Require Import String Lists.List. Import ListNotations. Notation var := string. diff --git a/src/verified_scheduling/codegen/.Makefileg.coq.d b/src/verified_scheduling/codegen/.Makefileg.coq.d deleted file mode 100644 index ca588ba..0000000 --- a/src/verified_scheduling/codegen/.Makefileg.coq.d +++ /dev/null @@ -1,18 +0,0 @@ -IdentParsing.vo IdentParsing.glob IdentParsing.v.beautified IdentParsing.required_vo: IdentParsing.v -IdentParsing.vio: IdentParsing.v -IdentParsing.vos IdentParsing.vok IdentParsing.required_vos: IdentParsing.v -Normalize.vo Normalize.glob Normalize.v.beautified Normalize.required_vo: Normalize.v ../atl/ATL.vo ../atl/Tactics.vo ../atl/Common.vo ../atl/CommonTactics.vo ../atl/Div.vo ../atl/GenPushout.vo ../atl/Reshape.vo ../atl/LetLifting.vo IdentParsing.vo -Normalize.vio: Normalize.v ../atl/ATL.vio ../atl/Tactics.vio ../atl/Common.vio ../atl/CommonTactics.vio ../atl/Div.vio ../atl/GenPushout.vio ../atl/Reshape.vio ../atl/LetLifting.vio IdentParsing.vio -Normalize.vos Normalize.vok Normalize.required_vos: Normalize.v ../atl/ATL.vos ../atl/Tactics.vos ../atl/Common.vos ../atl/CommonTactics.vos ../atl/Div.vos ../atl/GenPushout.vos ../atl/Reshape.vos ../atl/LetLifting.vos IdentParsing.vos -CheckSafe.vo CheckSafe.glob CheckSafe.v.beautified CheckSafe.required_vo: CheckSafe.v ../atl/ATL.vo ../atl/Tactics.vo ../atl/Div.vo ../atl/Common.vo ../atl/CommonTactics.vo ../../examples/Blur.vo -CheckSafe.vio: CheckSafe.v ../atl/ATL.vio ../atl/Tactics.vio ../atl/Div.vio ../atl/Common.vio ../atl/CommonTactics.vio ../../examples/Blur.vio -CheckSafe.vos CheckSafe.vok CheckSafe.required_vos: CheckSafe.v ../atl/ATL.vos ../atl/Tactics.vos ../atl/Div.vos ../atl/Common.vos ../atl/CommonTactics.vos ../../examples/Blur.vos -NatToString.vo NatToString.glob NatToString.v.beautified NatToString.required_vo: NatToString.v -NatToString.vio: NatToString.v -NatToString.vos NatToString.vok NatToString.required_vos: NatToString.v -IntToString.vo IntToString.glob IntToString.v.beautified IntToString.required_vo: IntToString.v -IntToString.vio: IntToString.v -IntToString.vos IntToString.vok IntToString.required_vos: IntToString.v -CodeGen.vo CodeGen.glob CodeGen.v.beautified CodeGen.required_vo: CodeGen.v ../atl/ATL.vo ../atl/Common.vo ../atl/CommonTactics.vo ../atl/Div.vo IdentParsing.vo NatToString.vo IntToString.vo Normalize.vo -CodeGen.vio: CodeGen.v ../atl/ATL.vio ../atl/Common.vio ../atl/CommonTactics.vio ../atl/Div.vio IdentParsing.vio NatToString.vio IntToString.vio Normalize.vio -CodeGen.vos CodeGen.vok CodeGen.required_vos: CodeGen.v ../atl/ATL.vos ../atl/Common.vos ../atl/CommonTactics.vos ../atl/Div.vos IdentParsing.vos NatToString.vos IntToString.vos Normalize.vos diff --git a/src/verified_scheduling/codegen/IdentParsing.v b/src/verified_scheduling/codegen/IdentParsing.v index 1afb80e..88b59a4 100644 --- a/src/verified_scheduling/codegen/IdentParsing.v +++ b/src/verified_scheduling/codegen/IdentParsing.v @@ -1,12 +1,12 @@ (*! Frontend | Ltac2-based identifier parsing for prettier notations !*) -Require Import Coq.NArith.NArith Coq.Strings.String. -Require Import Coq.Init.Byte. +From Stdlib Require Import NArith.NArith Strings.String. +From Stdlib Require Import Init.Byte. Require Import Ltac2.Ltac2. Import Ltac2.Init. Import Ltac2.Notations. -Import Coq.Lists.List.ListNotations. +Import Stdlib.Lists.List.ListNotations. Open Scope list. Ltac2 compute c := diff --git a/src/verified_scheduling/codegen/IntToString.v b/src/verified_scheduling/codegen/IntToString.v index 441470b..ea41f2e 100644 --- a/src/verified_scheduling/codegen/IntToString.v +++ b/src/verified_scheduling/codegen/IntToString.v @@ -3,7 +3,7 @@ From Stdlib Require Import ZArith.Zdiv. From Stdlib Require Import ZArith.Int. From Stdlib Require Import ZArith.Znat. -Require Import Coq.Strings.String. +From Stdlib Require Import Strings.String. Open Scope Z_scope. @@ -22,7 +22,7 @@ Definition int_to_ascii (n : Z) : ascii := end. Fixpoint int_to_string' (time: nat) (n : Z) (acc : string) : string := - let acc' := String (int_to_ascii (Coq.ZArith.BinIntDef.Z.modulo n 10)) acc in + let acc' := String (int_to_ascii (Stdlib.ZArith.BinIntDef.Z.modulo n 10)) acc in match time with | 0%nat => acc' | S time' => diff --git a/src/verified_scheduling/codegen/Makefileg.coq b/src/verified_scheduling/codegen/Makefileg.coq deleted file mode 100644 index 04bc116..0000000 --- a/src/verified_scheduling/codegen/Makefileg.coq +++ /dev/null @@ -1,989 +0,0 @@ -########################################################################## -## # The Coq Proof Assistant / The Coq Development Team ## -## v # Copyright INRIA, CNRS and contributors ## -## /dev/null 2>/dev/null; echo $$?)) -STDTIME?=command time -f $(TIMEFMT) -else -ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?)) -STDTIME?=gtime -f $(TIMEFMT) -else -STDTIME?=command time -endif -endif -else -STDTIME?=command time -f $(TIMEFMT) -endif - -COQBIN?= -ifneq (,$(COQBIN)) -# add an ending / -COQBIN:=$(COQBIN)/ -endif - -# Coq binaries -COQC ?= "$(COQBIN)coqc" -COQTOP ?= "$(COQBIN)coqtop" -COQCHK ?= "$(COQBIN)coqchk" -COQNATIVE ?= "$(COQBIN)coqnative" -COQDEP ?= "$(COQBIN)coqdep" -COQDOC ?= "$(COQBIN)coqdoc" -COQPP ?= "$(COQBIN)coqpp" -COQMKFILE ?= "$(COQBIN)coq_makefile" -OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" - -# Timing scripts -COQMAKE_ONE_TIME_FILE ?= "$(COQCORELIB)/tools/make-one-time-file.py" -COQMAKE_BOTH_TIME_FILES ?= "$(COQCORELIB)/tools/make-both-time-files.py" -COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQCORELIB)/tools/make-both-single-timing-files.py" -BEFORE ?= -AFTER ?= - -# OCaml binaries -CAMLC ?= "$(OCAMLFIND)" ocamlc -c -CAMLOPTC ?= "$(OCAMLFIND)" opt -c -CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkall -CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkall -CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack - -# DESTDIR is prepended to all installation paths -DESTDIR ?= - -# Debug builds, typically -g to OCaml, -debug to Coq. -CAMLDEBUG ?= -COQDEBUG ?= - -# Extra packages to be linked in (as in findlib -package) -CAMLPKGS ?= -FINDLIBPKGS = -package coq-core.plugins.ltac $(CAMLPKGS) - -# Option for making timing files -TIMING?= -# Option for changing sorting of timing output file -TIMING_SORT_BY ?= auto -# Option for changing the fuzz parameter on the output file -TIMING_FUZZ ?= 0 -# Option for changing whether to use real or user time for timing tables -TIMING_REAL?= -# Option for including the memory column(s) -TIMING_INCLUDE_MEM?= -# Option for sorting by the memory column -TIMING_SORT_BY_MEM?= -# Output file names for timed builds -TIME_OF_BUILD_FILE ?= time-of-build.log -TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log -TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log -TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log -TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log -TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line - -TGTS ?= - -# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) -ifdef DSTROOT -DESTDIR := $(DSTROOT) -endif - -# Substitution of the path by appending $(DESTDIR) if needed. -# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments. -windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1)) -destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1)) - -# Installation paths of libraries and documentation. -COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib) -COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/coq/user-contrib) -COQPLUGININSTALL ?= $(call destination_path,$(COQCORELIB)/..) -COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable? - -# findlib files installation -FINDLIBPREINST= mkdir -p "$(COQPLUGININSTALL)/" -FINDLIBDESTDIR= -destdir "$(COQPLUGININSTALL)/" - -# we need to move out of sight $(METAFILE) otherwise findlib thinks the -# package is already installed -findlib_install = \ - $(HIDE)if [ "$(METAFILE)" ]; then \ - $(FINDLIBPREINST) && \ - mv "$(METAFILE)" "$(METAFILE).skip" ; \ - "$(OCAMLFIND)" install $(2) $(FINDLIBDESTDIR) $(FINDLIBPACKAGE) $(1); \ - rc=$$?; \ - mv "$(METAFILE).skip" "$(METAFILE)"; \ - exit $$rc; \ - fi -findlib_remove = \ - $(HIDE)if [ ! -z "$(METAFILE)" ]; then\ - "$(OCAMLFIND)" remove $(FINDLIBDESTDIR) $(FINDLIBPACKAGE); \ - fi - - -########## End of parameters ################################################## -# What follows may be relevant to you only if you need to -# extend this Makefile. If so, look for 'Extension point' here and -# put in Makefileg.coq.local double colon rules accordingly. -# E.g. to perform some work after the all target completes you can write -# -# post-all:: -# echo "All done!" -# -# in Makefileg.coq.local -# -############################################################################### - - - - -# Flags ####################################################################### -# -# We define a bunch of variables combining the parameters. -# To add additional flags to coq, coqchk or coqdoc, set the -# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add. -# To overwrite the default choice and set your own flags entirely, set the -# {COQ,COQCHK,COQDOC}FLAGS variable. - -SHOW := $(if $(VERBOSE),@true "",@echo "") -HIDE := $(if $(VERBOSE),,@) - -TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) - -OPT?= - -# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d -ifeq '$(OPT)' '-byte' -USEBYTE:=true -DYNOBJ:=.cma -DYNLIB:=.cma -else -USEBYTE:= -DYNOBJ:=.cmxs -DYNLIB:=.cmxs -endif - -# these variables are meant to be overridden if you want to add *extra* flags -COQEXTRAFLAGS?= -COQCHKEXTRAFLAGS?= -COQDOCEXTRAFLAGS?= - -# Find the last argument of the form "-native-compiler FLAG" -COQUSERNATIVEFLAG:=$(strip \ -$(subst -native-compiler-,,\ -$(lastword \ -$(filter -native-compiler-%,\ -$(subst -native-compiler ,-native-compiler-,\ -$(strip $(COQEXTRAFLAGS))))))) - -COQFILTEREDEXTRAFLAGS:=$(strip \ -$(filter-out -native-compiler-%,\ -$(subst -native-compiler ,-native-compiler-,\ -$(strip $(COQEXTRAFLAGS))))) - -COQACTUALNATIVEFLAG:=$(lastword $(COQMF_COQ_NATIVE_COMPILER_DEFAULT) $(COQMF_COQPROJECTNATIVEFLAG) $(COQUSERNATIVEFLAG)) - -ifeq '$(COQACTUALNATIVEFLAG)' 'yes' - COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" - COQDONATIVE="yes" -else -ifeq '$(COQACTUALNATIVEFLAG)' 'ondemand' - COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" - COQDONATIVE="no" -else - COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "no" - COQDONATIVE="no" -endif -endif - -# these flags do NOT contain the libraries, to make them easier to overwrite -COQFLAGS?=-q $(OTHERFLAGS) $(COQFILTEREDEXTRAFLAGS) $(COQNATIVEFLAG) -COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) -COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) - -COQDOCLIBS?=$(COQLIBS_NOML) - -# The version of Coq being run and the version of coq_makefile that -# generated this makefile -COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) -COQMAKEFILE_VERSION:=8.18.0 - -# COQ_SRC_SUBDIRS is for user-overriding, usually to add -# `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for -# Coq's own core libraries, which should be replaced by ocamlfind -# options at some point. -COQ_SRC_SUBDIRS?= -COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") - -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -# ocamldoc fails with unknown argument otherwise -CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) -CAMLFLAGS+=$(OCAMLWARN) - -ifneq (,$(TIMING)) - ifeq (after,$(TIMING)) - TIMING_EXT=after-timing - else - ifeq (before,$(TIMING)) - TIMING_EXT=before-timing - else - TIMING_EXT=timing - endif - endif - TIMING_ARG=-time-file $<.$(TIMING_EXT) -else - TIMING_ARG= -endif - -# Files ####################################################################### -# -# We here define a bunch of variables about the files being part of the -# Coq project in order to ease the writing of build target and build rules - -VDFILE := .Makefileg.coq.d - -ALLSRCFILES := \ - $(MLGFILES) \ - $(MLFILES) \ - $(MLPACKFILES) \ - $(MLLIBFILES) \ - $(MLIFILES) - -# helpers -vo_to_obj = $(addsuffix .o,\ - $(filter-out Warning: Error:,\ - $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) -strip_dotslash = $(patsubst ./%,%,$(1)) - -# without this we get undefined variables in the expansion for the -# targets of the [deprecated,use-mllib-or-mlpack] rule -with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) - -VO = vo -VOS = vos - -VOFILES = $(VFILES:.v=.$(VO)) -GLOBFILES = $(VFILES:.v=.glob) -HTMLFILES = $(VFILES:.v=.html) -GHTMLFILES = $(VFILES:.v=.g.html) -BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) -TEXFILES = $(VFILES:.v=.tex) -GTEXFILES = $(VFILES:.v=.g.tex) -CMOFILES = \ - $(MLGFILES:.mlg=.cmo) \ - $(MLFILES:.ml=.cmo) \ - $(MLPACKFILES:.mlpack=.cmo) -CMXFILES = $(CMOFILES:.cmo=.cmx) -OFILES = $(CMXFILES:.cmx=.o) -CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) -CMXAFILES = $(CMAFILES:.cma=.cmxa) -CMIFILES = \ - $(CMOFILES:.cmo=.cmi) \ - $(MLIFILES:.mli=.cmi) -# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just -# a .mlg file -CMXSFILES = \ - $(MLPACKFILES:.mlpack=.cmxs) \ - $(CMXAFILES:.cmxa=.cmxs) \ - $(if $(MLPACKFILES)$(CMXAFILES),,\ - $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs)) - -# files that are packed into a plugin (no extension) -PACKEDFILES = \ - $(call strip_dotslash, \ - $(foreach lib, \ - $(call strip_dotslash, \ - $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib)))) -# files that are archived into a .cma (mllib) -LIBEDFILES = \ - $(call strip_dotslash, \ - $(foreach lib, \ - $(call strip_dotslash, \ - $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib)))) -CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) -CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) -OBJFILES = $(call vo_to_obj,$(VOFILES)) -ALLNATIVEFILES = \ - $(OBJFILES:.o=.cmi) \ - $(OBJFILES:.o=.cmx) \ - $(OBJFILES:.o=.cmxs) -FINDLIBPACKAGE=$(patsubst .%,%,$(suffix $(METAFILE))) - -# trick: wildcard filters out non-existing files, so that `install` doesn't show -# warnings and `clean` doesn't pass to rm a list of files that is too long for -# the shell. -NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) -FILESTOINSTALL = \ - $(VOFILES) \ - $(VFILES) \ - $(GLOBFILES) \ - $(NATIVEFILES) \ - $(CMXSFILES) # to be removed when we remove legacy loading -FINDLIBFILESTOINSTALL = \ - $(CMIFILESTOINSTALL) -ifeq '$(HASNATDYNLINK)' 'true' -DO_NATDYNLINK = yes -FINDLIBFILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx) -else -DO_NATDYNLINK = -endif - -ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE) - -# Compilation targets ######################################################### - -all: - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all -.PHONY: all - -all.timing.diff: - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES="" - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all -.PHONY: all.timing.diff - -ifeq (0,$(TIMING_REAL)) -TIMING_REAL_ARG := -TIMING_USER_ARG := --user -else -ifeq (1,$(TIMING_REAL)) -TIMING_REAL_ARG := --real -TIMING_USER_ARG := -else -TIMING_REAL_ARG := -TIMING_USER_ARG := -endif -endif - -ifeq (0,$(TIMING_INCLUDE_MEM)) -TIMING_INCLUDE_MEM_ARG := --no-include-mem -else -TIMING_INCLUDE_MEM_ARG := -endif - -ifeq (1,$(TIMING_SORT_BY_MEM)) -TIMING_SORT_BY_MEM_ARG := --sort-by-mem -else -TIMING_SORT_BY_MEM_ARG := -endif - -make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) -make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) -make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: - $(HIDE)rm -f pretty-timed-success.ok - $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) - $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed -print-pretty-timed:: - $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) -print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) -ifeq (,$(BEFORE)) -print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' - $(HIDE)false -else -ifeq (,$(AFTER)) -print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' - $(HIDE)false -else -print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) -endif -endif -pretty-timed: - $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed -.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff - -# Extension points for actions to be performed before/after the all target -pre-all:: - @# Extension point - $(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\ - echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\ - echo "W: while the current Coq version is $(COQ_VERSION)";\ - fi -.PHONY: pre-all - -post-all:: - @# Extension point -.PHONY: post-all - -real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) -.PHONY: real-all - -real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) -.PHONY: real-all.timing.diff - -bytefiles: $(CMOFILES) $(CMAFILES) -.PHONY: bytefiles - -optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) -.PHONY: optfiles - -# FIXME, see Ralf's bugreport -# quick is deprecated, now renamed vio -vio: $(VOFILES:.vo=.vio) -.PHONY: vio -quick: vio - $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") -.PHONY: quick - -vio2vo: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ - -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) -.PHONY: vio2vo - -# quick2vo is undocumented -quick2vo: - $(HIDE)make -j $(J) vio - $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ - viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ - if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ - done); \ - echo "VIO2VO: $$VIOFILES"; \ - if [ -n "$$VIOFILES" ]; then \ - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \ - fi -.PHONY: quick2vo - -checkproofs: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ - -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) -.PHONY: checkproofs - -vos: $(VOFILES:%.vo=%.vos) -.PHONY: vos - -vok: $(VOFILES:%.vo=%.vok) -.PHONY: vok - -validate: $(VOFILES) - $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^ -.PHONY: validate - -only: $(TGTS) -.PHONY: only - -# Documentation targets ####################################################### - -html: $(GLOBFILES) $(VFILES) - $(SHOW)'COQDOC -d html $(GAL)' - $(HIDE)mkdir -p html - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES) - -mlihtml: $(MLIFILES:.mli=.cmi) - $(SHOW)'CAMLDOC -d $@' - $(HIDE)mkdir $@ || rm -rf $@/* - $(HIDE)$(CAMLDOC) -html \ - -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) - -all-mli.tex: $(MLIFILES:.mli=.cmi) - $(SHOW)'CAMLDOC -latex $@' - $(HIDE)$(CAMLDOC) -latex \ - -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) - -all.ps: $(VFILES) - $(SHOW)'COQDOC -ps $(GAL)' - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort $(VFILES)` - -all.pdf: $(VFILES) - $(SHOW)'COQDOC -pdf $(GAL)' - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort $(VFILES)` - -# FIXME: not quite right, since the output name is different -gallinahtml: GAL=-g -gallinahtml: html - -all-gal.ps: GAL=-g -all-gal.ps: all.ps - -all-gal.pdf: GAL=-g -all-gal.pdf: all.pdf - -# ? -beautify: $(BEAUTYFILES) - for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done - @echo 'Do not do "make clean" until you are sure that everything went well!' - @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' -.PHONY: beautify - -# Installation targets ######################################################## -# -# There rules can be extended in Makefileg.coq.local -# Extensions can't assume when they run. - -# We use $(file) to avoid generating a very long command string to pass to the shell -# (cf https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform-devs-.26-users/topic/Strange.20command.20length.20limit.20on.20Linux) -# However Apple ships old make which doesn't have $(file) so we need a fallback -$(file >.hasfile,1) -HASFILE:=$(shell if [ -e .hasfile ]; then echo 1; rm .hasfile; fi) - -MKFILESTOINSTALL= $(if $(HASFILE),$(file >.filestoinstall,$(FILESTOINSTALL)),\ - $(shell rm -f .filestoinstall) \ - $(foreach x,$(FILESTOINSTALL),$(shell printf '%s\n' "$x" >> .filestoinstall))) - -# findlib needs the package to not be installed, so we remove it before -# installing it (see the call to findlib_remove) -install: META - @$(MKFILESTOINSTALL) - $(HIDE)code=0; for f in $$(cat .filestoinstall); do\ - if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ - done; exit $$code - $(HIDE)for f in $$(cat .filestoinstall); do\ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ - if [ "$$?" != "0" -o -z "$$df" ]; then\ - echo SKIP "$$f" since it has no logical path;\ - else\ - install -d "$(COQLIBINSTALL)/$$df" &&\ - install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ - echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ - fi;\ - done - $(call findlib_remove) - $(call findlib_install, META $(FINDLIBFILESTOINSTALL)) - $(HIDE)$(MAKE) install-extra -f "$(SELF)" - @rm -f .filestoinstall -install-extra:: - @# Extension point -.PHONY: install install-extra - -META: $(METAFILE) - $(HIDE)if [ "$(METAFILE)" ]; then \ - cat "$(METAFILE)" | grep -v 'directory.*=.*' > META; \ - fi - -install-byte: - $(call findlib_install, $(CMAFILES) $(CMOFILESTOINSTALL), -add) - -install-doc:: html mlihtml - @# Extension point - $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" - $(HIDE)for i in html/*; do \ - dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ - install -m 0644 "$$i" "$$dest";\ - echo INSTALL "$$i" "$$dest";\ - done - $(HIDE)install -d \ - "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE)for i in mlihtml/*; do \ - dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ - install -m 0644 "$$i" "$$dest";\ - echo INSTALL "$$i" "$$dest";\ - done -.PHONY: install-doc - -uninstall:: - @# Extension point - @$(MKFILESTOINSTALL) - $(call findlib_remove) - $(HIDE)for f in $$(cat .filestoinstall); do \ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ - instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ - rm -f "$$instf" &&\ - echo RM "$$instf" ;\ - done - $(HIDE)for f in $$(cat .filestoinstall); do \ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ - echo RMDIR "$(COQLIBINSTALL)/$$df/" &&\ - (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \ - done - @rm -f .filestoinstall - -.PHONY: uninstall - -uninstall-doc:: - @# Extension point - $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' - $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" - $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' - $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true -.PHONY: uninstall-doc - -# Cleaning #################################################################### -# -# There rules can be extended in Makefileg.coq.local -# Extensions can't assume when they run. - -clean:: - @# Extension point - $(SHOW)'CLEAN' - $(HIDE)rm -f $(CMOFILES) - $(HIDE)rm -f $(CMIFILES) - $(HIDE)rm -f $(CMAFILES) - $(HIDE)rm -f $(CMXFILES) - $(HIDE)rm -f $(CMXAFILES) - $(HIDE)rm -f $(CMXSFILES) - $(HIDE)rm -f $(OFILES) - $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) - $(HIDE)rm -f $(MLGFILES:.mlg=.ml) - $(HIDE)rm -f $(CMXFILES:.cmx=.cmt) - $(HIDE)rm -f $(MLIFILES:.mli=.cmti) - $(HIDE)rm -f $(ALLDFILES) - $(HIDE)rm -f $(NATIVEFILES) - $(HIDE)find . -name .coq-native -type d -empty -delete - $(HIDE)rm -f $(VOFILES) - $(HIDE)rm -f $(VOFILES:.vo=.vio) - $(HIDE)rm -f $(VOFILES:.vo=.vos) - $(HIDE)rm -f $(VOFILES:.vo=.vok) - $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) - $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex - $(HIDE)rm -f $(VFILES:.v=.glob) - $(HIDE)rm -f $(VFILES:.v=.tex) - $(HIDE)rm -f $(VFILES:.v=.g.tex) - $(HIDE)rm -f pretty-timed-success.ok - $(HIDE)rm -f META - $(HIDE)rm -rf html mlihtml -.PHONY: clean - -cleanall:: clean - @# Extension point - $(SHOW)'CLEAN *.aux *.timing' - $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) - $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) - $(HIDE)rm -f $(VOFILES:.vo=.v.timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) - $(HIDE)rm -f .lia.cache .nia.cache -.PHONY: cleanall - -archclean:: - @# Extension point - $(SHOW)'CLEAN *.cmx *.o' - $(HIDE)rm -f $(NATIVEFILES) - $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) -.PHONY: archclean - - -# Compilation rules ########################################################### - -$(MLIFILES:.mli=.cmi): %.cmi: %.mli - $(SHOW)'CAMLC -c $<' - $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< - -$(MLGFILES:.mlg=.ml): %.ml: %.mlg - $(SHOW)'COQPP $<' - $(HIDE)$(COQPP) $< - -# Stupid hack around a deficient syntax: we cannot concatenate two expansions -$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml - $(SHOW)'CAMLC -c $<' - $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< - -# Same hack -$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml - $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' - $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $(FOR_PACK) $< - - -$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa - $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ - -shared -o $@ $< - -$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib - $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ - -$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib - $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ - - -$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa - $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ - -shared -o $@ $< - -$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx | %.mlpack - $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $< - -$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack - $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ - -$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack - $(SHOW)'CAMLC -pack -o $@' - $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^ - -$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack - $(SHOW)'CAMLOPT -pack -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^ - -# This rule is for _CoqProject with no .mllib nor .mlpack -$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx - $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ - -shared -o $@ $< - -# can't make -# https://www.gnu.org/software/make/manual/make.html#Static-Pattern -# work with multiple target rules -# so use eval in a loop instead -# with grouped targets https://www.gnu.org/software/make/manual/make.html#Multiple-Targets -# if available (GNU Make >= 4.3) -ifneq (,$(filter grouped-target,$(.FEATURES))) -define globvorule= - -# take care to $$ variables using $< etc - $(1).vo $(1).glob &: $(1).v | $(VDFILE) - $(SHOW)COQC $(1).v - $(HIDE)$$(TIMER) $(COQC) $(COQDEBUG) $$(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $(1).v -ifeq ($(COQDONATIVE), "yes") - $(SHOW)COQNATIVE $(1).vo - $(HIDE)$(call TIMER,$(1).vo.native) $(COQNATIVE) $(COQLIBS) $(1).vo -endif - -endef -else - -$(VOFILES): %.vo: %.v | $(VDFILE) - $(SHOW)COQC $< - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< -ifeq ($(COQDONATIVE), "yes") - $(SHOW)COQNATIVE $@ - $(HIDE)$(call TIMER,$@.native) $(COQNATIVE) $(COQLIBS) $@ -endif - -# this is broken :( todo fix if we ever find a solution that doesn't need grouped targets -$(GLOBFILES): %.glob: %.v - $(SHOW)'COQC $< (for .glob)' - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -endif - -$(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile)))) - -$(VFILES:.v=.vio): %.vio: %.v - $(SHOW)COQC -vio $< - $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -$(VFILES:.v=.vos): %.vos: %.v - $(SHOW)COQC -vos $< - $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -$(VFILES:.v=.vok): %.vok: %.v - $(SHOW)COQC -vok $< - $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing - $(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" - -$(BEAUTYFILES): %.v.beautified: %.v - $(SHOW)'BEAUTIFY $<' - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $< - -$(TEXFILES): %.tex: %.v - $(SHOW)'COQDOC -latex $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ - -$(GTEXFILES): %.g.tex: %.v - $(SHOW)'COQDOC -latex -g $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ - -$(HTMLFILES): %.html: %.v %.glob - $(SHOW)'COQDOC -html $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@ - -$(GHTMLFILES): %.g.html: %.v %.glob - $(SHOW)'COQDOC -html -g $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ - -# Dependency files ############################################################ - -ifndef MAKECMDGOALS - -include $(ALLDFILES) -else - ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) - -include $(ALLDFILES) - endif -endif - -.SECONDARY: $(ALLDFILES) - -redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) - -GENMLFILES:=$(MLGFILES:.mlg=.ml) -$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES) - -$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) - -# If this makefile is created using a _CoqProject we have coqdep get -# options from it. This avoids argument length limits for pathological -# projects. Note that extra options might be on the command line. -VDFILE_FLAGS:=$(if ,-f ,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) - -$(VDFILE): $(VFILES) - $(SHOW)'COQDEP VFILES' - $(HIDE)$(COQDEP) $(if $(strip $(METAFILE)),-m "$(METAFILE)") -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) - -# Misc ######################################################################## - -byte: - $(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)" -.PHONY: byte - -opt: - $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)" -.PHONY: opt - -# This is deprecated. To extend this makefile use -# extension points and Makefileg.coq.local -printenv:: - $(warning printenv is deprecated) - $(warning write extensions in Makefileg.coq.local or include Makefileg.coq.conf) - @echo 'COQLIB = $(COQLIB)' - @echo 'COQCORELIB = $(COQCORELIB)' - @echo 'DOCDIR = $(DOCDIR)' - @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' - @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' - @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' - @echo 'COQCORE_SRC_SUBDIRS = $(COQCORE_SRC_SUBDIRS)' - @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'PP = $(PP)' - @echo 'COQFLAGS = $(COQFLAGS)' - @echo 'COQLIB = $(COQLIBS)' - @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' - @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' -.PHONY: printenv - -# Generate a .merlin file. If you need to append directives to this -# file you can extend the merlin-hook target in Makefileg.coq.local -.merlin: - $(SHOW)'FILL .merlin' - $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin - $(HIDE)echo 'B $(COQCORELIB)' >> .merlin - $(HIDE)echo 'S $(COQCORELIB)' >> .merlin - $(HIDE)$(foreach d,$(COQCORE_SRC_SUBDIRS), \ - echo 'B $(COQCORELIB)$(d)' >> .merlin;) - $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo 'S $(COQLIB)$(d)' >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) - $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" -.PHONY: merlin - -merlin-hook:: - @# Extension point -.PHONY: merlin-hook - -# prints all variables -debug: - $(foreach v,\ - $(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\ - $(.VARIABLES))),\ - $(info $(v) = $($(v)))) -.PHONY: debug - -.DEFAULT_GOAL := all - -# Users can create Makefileg.coq.local-late to hook into double-colon rules -# or add other needed Makefile code, using defined -# variables if necessary. --include Makefileg.coq.local-late - -# Local Variables: -# mode: makefile-gmake -# End: diff --git a/src/verified_scheduling/codegen/Makefileg.coq.conf b/src/verified_scheduling/codegen/Makefileg.coq.conf deleted file mode 100644 index f8611cc..0000000 --- a/src/verified_scheduling/codegen/Makefileg.coq.conf +++ /dev/null @@ -1,71 +0,0 @@ -# This configuration file was generated by running: -# coq_makefile -R ../atl ATL -R ../../examples Examples -R . Codegen IdentParsing.v Normalize.v CheckSafe.v NatToString.v IntToString.v CodeGen.v -o Makefileg.coq - -COQBIN?= -ifneq (,$(COQBIN)) -# add an ending / -COQBIN:=$(COQBIN)/ -endif -COQMKFILE ?= "$(COQBIN)coq_makefile" - -############################################################################### -# # -# Project files. # -# # -############################################################################### - -COQMF_CMDLINE_VFILES := IdentParsing.v Normalize.v CheckSafe.v NatToString.v IntToString.v CodeGen.v -COQMF_SOURCES := $(shell $(COQMKFILE) -sources-of $(COQMF_CMDLINE_VFILES)) -COQMF_VFILES := $(filter %.v, $(COQMF_SOURCES)) -COQMF_MLIFILES := $(filter %.mli, $(COQMF_SOURCES)) -COQMF_MLFILES := $(filter %.ml, $(COQMF_SOURCES)) -COQMF_MLGFILES := $(filter %.mlg, $(COQMF_SOURCES)) -COQMF_MLPACKFILES := $(filter %.mlpack, $(COQMF_SOURCES)) -COQMF_MLLIBFILES := $(filter %.mllib, $(COQMF_SOURCES)) -COQMF_METAFILE = - -############################################################################### -# # -# Path directives (-I, -R, -Q). # -# # -############################################################################### - -COQMF_OCAMLLIBS = -COQMF_SRC_SUBDIRS = -COQMF_COQLIBS = -R ../atl ATL -R ../../examples Examples -R . Codegen -COQMF_COQLIBS_NOML = -R ../atl ATL -R ../../examples Examples -R . Codegen -COQMF_CMDLINE_COQLIBS = -R ../atl ATL -R ../../examples Examples -R . Codegen - -############################################################################### -# # -# Coq configuration. # -# # -############################################################################### - -COQMF_COQLIB=/home/lamanda/.opam/ocaml-base-compiler/lib/coq/ -COQMF_COQCORELIB=/home/lamanda/.opam/ocaml-base-compiler/lib/coq/../coq-core/ -COQMF_DOCDIR=/home/lamanda/.opam/ocaml-base-compiler/share/doc/ -COQMF_OCAMLFIND=/home/lamanda/.opam/ocaml-base-compiler/bin/ocamlfind -COQMF_CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -COQMF_WARN=-warn-error +a-3 -COQMF_HASNATDYNLINK=true -COQMF_COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax -COQMF_COQ_NATIVE_COMPILER_DEFAULT=no -COQMF_WINDRIVE= - -############################################################################### -# # -# Native compiler. # -# # -############################################################################### - -COQMF_COQPROJECTNATIVEFLAG = - -############################################################################### -# # -# Extra variables. # -# # -############################################################################### - -COQMF_OTHERFLAGS = -COQMF_INSTALLCOQDOCROOT = orphan_ATL_Examples_Codegen diff --git a/src/verified_scheduling/codegen/NatToString.v b/src/verified_scheduling/codegen/NatToString.v index fb15c96..e80b4a0 100644 --- a/src/verified_scheduling/codegen/NatToString.v +++ b/src/verified_scheduling/codegen/NatToString.v @@ -1,5 +1,5 @@ From Stdlib Require Import Ascii String Arith. -Require Import Coq.Strings.String. +From Stdlib Require Import Strings.String. Definition nat_to_ascii (n : nat) : ascii := match n with From 6b00ee2b4461d908c8da588bdec5d3e009efe1e4 Mon Sep 17 00:00:00 2001 From: Owen Conoly Date: Tue, 14 Oct 2025 14:02:54 -0400 Subject: [PATCH 5/5] make gitignore ignore files generated by make --- .gitignore | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index cd31931..16fa114 100644 --- a/.gitignore +++ b/.gitignore @@ -5,4 +5,4 @@ src/clib/* *.v.d *.aux .lia.cache -Makefile.coq +**Makefile*coq*