diff options
author | Jason Gross <jgross@mit.edu> | 2017-01-19 14:05:54 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-01-19 14:05:54 -0500 |
commit | cded6731f79a66018d3660017bda7a284aedf50c (patch) | |
tree | 1311ed7d6d0bf9a06a5ad86531a708de4e95e19d | |
parent | cb98e6d8a45b68e29546732a0eed969c724a0274 (diff) |
Split out Reflection.Equality, change Tflat implicit argument
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/Reflection/Equality.v | 92 | ||||
-rw-r--r-- | src/Reflection/MapCastWithCastOp.v | 1 | ||||
-rw-r--r-- | src/Reflection/MultiSizeTest2.v | 1 | ||||
-rw-r--r-- | src/Reflection/Syntax.v | 84 | ||||
-rw-r--r-- | src/Reflection/TestCase.v | 5 | ||||
-rw-r--r-- | src/Reflection/Z/Syntax.v | 1 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Common.v | 4 | ||||
-rw-r--r-- | src/SpecificGen/GF2213_32Reflective/Common.v | 4 | ||||
-rw-r--r-- | src/SpecificGen/GF2519_32Reflective/Common.v | 4 | ||||
-rw-r--r-- | src/SpecificGen/GF25519_32Reflective/Common.v | 4 | ||||
-rw-r--r-- | src/SpecificGen/GF25519_64Reflective/Common.v | 4 | ||||
-rw-r--r-- | src/SpecificGen/GF41417_32Reflective/Common.v | 4 | ||||
-rw-r--r-- | src/SpecificGen/GF5211_32Reflective/Common.v | 4 |
14 files changed, 114 insertions, 99 deletions
diff --git a/_CoqProject b/_CoqProject index a386dc91c..d7a41d4d7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -100,6 +100,7 @@ src/Reflection/ApplicationRelations.v src/Reflection/CommonSubexpressionElimination.v src/Reflection/Conversion.v src/Reflection/CountLets.v +src/Reflection/Equality.v src/Reflection/ExprInversion.v src/Reflection/FilterLive.v src/Reflection/Inline.v diff --git a/src/Reflection/Equality.v b/src/Reflection/Equality.v new file mode 100644 index 000000000..39d2675b5 --- /dev/null +++ b/src/Reflection/Equality.v @@ -0,0 +1,92 @@ +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Util.Decidable. + +Section language. + Context (base_type_code : Type) + (eq_base_type_code : base_type_code -> base_type_code -> bool) + (base_type_code_bl : forall x y, eq_base_type_code x y = true -> x = y) + (base_type_code_lb : forall x y, x = y -> eq_base_type_code x y = true). + + Local Notation flat_type := (flat_type base_type_code). + Local Notation type := (type base_type_code). + + Fixpoint flat_type_beq (X Y : flat_type) {struct X} : bool + := match X, Y with + | Tbase T, Tbase T0 => eq_base_type_code T T0 + | Prod A B, Prod A0 B0 => (flat_type_beq A A0 && flat_type_beq B B0)%bool + | Tbase _, _ + | Prod _ _, _ + => false + end. + Local Ltac t := + repeat match goal with + | _ => intro + | _ => reflexivity + | _ => assumption + | _ => progress simpl in * + | _ => solve [ eauto with nocore ] + | [ H : False |- _ ] => exfalso; assumption + | [ H : false = true |- _ ] => apply Bool.diff_false_true in H + | [ |- Prod _ _ = Prod _ _ ] => apply f_equal2 + | [ |- Arrow _ _ = Arrow _ _ ] => apply f_equal2 + | [ |- Tbase _ = Tbase _ ] => apply f_equal + | [ |- Tflat _ = Tflat _ ] => apply f_equal + | [ H : forall Y, _ = true -> _ = Y |- _ = ?Y' ] + => is_var Y'; apply H; solve [ t ] + | [ H : forall X Y, X = Y -> _ = true |- _ = true ] + => eapply H; solve [ t ] + | [ H : true = true |- _ ] => clear H + | [ H : andb ?x ?y = true |- _ ] + => destruct x, y; simpl in H; solve [ t ] + | [ H : andb ?x ?y = true |- _ ] + => destruct x eqn:?; simpl in H + | [ H : ?f ?x = true |- _ ] => destruct (f x); solve [ t ] + | [ H : ?x = true |- andb _ ?x = true ] + => destruct x + | [ |- andb ?x true = true ] + => cut (x = true); [ destruct x; simpl | ] + end. + Lemma flat_type_dec_bl X : forall Y, flat_type_beq X Y = true -> X = Y. + Proof. clear base_type_code_lb; induction X, Y; t. Defined. + Lemma flat_type_dec_lb X : forall Y, X = Y -> flat_type_beq X Y = true. + Proof. clear base_type_code_bl; intros; subst Y; induction X; t. Defined. + Definition flat_type_eq_dec (X Y : flat_type) : {X = Y} + {X <> Y} + := match Sumbool.sumbool_of_bool (flat_type_beq X Y) with + | left pf => left (flat_type_dec_bl _ _ pf) + | right pf => right (fun pf' => let pf'' := eq_sym (flat_type_dec_lb _ _ pf') in + Bool.diff_true_false (eq_trans pf'' pf)) + end. + Fixpoint type_beq (X Y : type) {struct X} : bool + := match X, Y with + | Tflat T, Tflat T0 => flat_type_beq T T0 + | Arrow A B, Arrow A0 B0 => (eq_base_type_code A A0 && type_beq B B0)%bool + | Tflat _, _ + | Arrow _ _, _ + => false + end. + Lemma type_dec_bl X : forall Y, type_beq X Y = true -> X = Y. + Proof. clear base_type_code_lb; pose proof flat_type_dec_bl; induction X, Y; t. Defined. + Lemma type_dec_lb X : forall Y, X = Y -> type_beq X Y = true. + Proof. clear base_type_code_bl; pose proof flat_type_dec_lb; intros; subst Y; induction X; t. Defined. + Definition type_eq_dec (X Y : type) : {X = Y} + {X <> Y} + := match Sumbool.sumbool_of_bool (type_beq X Y) with + | left pf => left (type_dec_bl _ _ pf) + | right pf => right (fun pf' => let pf'' := eq_sym (type_dec_lb _ _ pf') in + Bool.diff_true_false (eq_trans pf'' pf)) + end. +End language. + +Lemma dec_eq_flat_type {base_type_code} `{DecidableRel (@eq base_type_code)} + : DecidableRel (@eq (flat_type base_type_code)). +Proof. + repeat intro; hnf; decide equality; apply dec; auto. +Defined. +Hint Extern 1 (Decidable (@eq (flat_type ?base_type_code) ?x ?y)) +=> simple apply (@dec_eq_flat_type base_type_code) : typeclass_instances. +Lemma dec_eq_type {base_type_code} `{DecidableRel (@eq base_type_code)} + : DecidableRel (@eq (type base_type_code)). +Proof. + repeat intro; hnf; decide equality; apply dec; typeclasses eauto. +Defined. +Hint Extern 1 (Decidable (@eq (type ?base_type_code) ?x ?y)) +=> simple apply (@dec_eq_type base_type_code) : typeclass_instances. diff --git a/src/Reflection/MapCastWithCastOp.v b/src/Reflection/MapCastWithCastOp.v index f896e71fb..189399fad 100644 --- a/src/Reflection/MapCastWithCastOp.v +++ b/src/Reflection/MapCastWithCastOp.v @@ -1,4 +1,5 @@ Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Equality. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.MapCast. Require Import Crypto.Util.Sigma. diff --git a/src/Reflection/MultiSizeTest2.v b/src/Reflection/MultiSizeTest2.v index a0c9fc864..8dbc8f4ce 100644 --- a/src/Reflection/MultiSizeTest2.v +++ b/src/Reflection/MultiSizeTest2.v @@ -1,5 +1,6 @@ Require Import Coq.omega.Omega. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Equality. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.MapCastWithCastOp. Require Import Crypto.Reflection.MapInterp. diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 3f1fec3c7..f8d7cdcf3 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -1,7 +1,6 @@ (** * PHOAS Representation of Gallina *) Require Import Coq.Strings.String Coq.Classes.RelationClasses Coq.Classes.Morphisms. Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.Decidable. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. @@ -23,77 +22,6 @@ Section language. Inductive type := Tflat (T : flat_type) | Arrow (A : base_type_code) (B : type). Bind Scope ctype_scope with type. - Section dec. - Context (eq_base_type_code : base_type_code -> base_type_code -> bool) - (base_type_code_bl : forall x y, eq_base_type_code x y = true -> x = y) - (base_type_code_lb : forall x y, x = y -> eq_base_type_code x y = true). - - Fixpoint flat_type_beq (X Y : flat_type) {struct X} : bool - := match X, Y with - | Tbase T, Tbase T0 => eq_base_type_code T T0 - | Prod A B, Prod A0 B0 => (flat_type_beq A A0 && flat_type_beq B B0)%bool - | Tbase _, _ - | Prod _ _, _ - => false - end. - Local Ltac t := - repeat match goal with - | _ => intro - | _ => reflexivity - | _ => assumption - | _ => progress simpl in * - | _ => solve [ eauto with nocore ] - | [ H : False |- _ ] => exfalso; assumption - | [ H : false = true |- _ ] => apply Bool.diff_false_true in H - | [ |- Prod _ _ = Prod _ _ ] => apply f_equal2 - | [ |- Arrow _ _ = Arrow _ _ ] => apply f_equal2 - | [ |- Tbase _ = Tbase _ ] => apply f_equal - | [ |- Tflat _ = Tflat _ ] => apply f_equal - | [ H : forall Y, _ = true -> _ = Y |- _ = ?Y' ] - => is_var Y'; apply H; solve [ t ] - | [ H : forall X Y, X = Y -> _ = true |- _ = true ] - => eapply H; solve [ t ] - | [ H : true = true |- _ ] => clear H - | [ H : andb ?x ?y = true |- _ ] - => destruct x, y; simpl in H; solve [ t ] - | [ H : andb ?x ?y = true |- _ ] - => destruct x eqn:?; simpl in H - | [ H : ?f ?x = true |- _ ] => destruct (f x); solve [ t ] - | [ H : ?x = true |- andb _ ?x = true ] - => destruct x - | [ |- andb ?x true = true ] - => cut (x = true); [ destruct x; simpl | ] - end. - Lemma flat_type_dec_bl X : forall Y, flat_type_beq X Y = true -> X = Y. - Proof. clear base_type_code_lb; induction X, Y; t. Defined. - Lemma flat_type_dec_lb X : forall Y, X = Y -> flat_type_beq X Y = true. - Proof. clear base_type_code_bl; intros; subst Y; induction X; t. Defined. - Definition flat_type_eq_dec (X Y : flat_type) : {X = Y} + {X <> Y} - := match Sumbool.sumbool_of_bool (flat_type_beq X Y) with - | left pf => left (flat_type_dec_bl _ _ pf) - | right pf => right (fun pf' => let pf'' := eq_sym (flat_type_dec_lb _ _ pf') in - Bool.diff_true_false (eq_trans pf'' pf)) - end. - Fixpoint type_beq (X Y : type) {struct X} : bool - := match X, Y with - | Tflat T, Tflat T0 => flat_type_beq T T0 - | Arrow A B, Arrow A0 B0 => (eq_base_type_code A A0 && type_beq B B0)%bool - | Tflat _, _ - | Arrow _ _, _ - => false - end. - Lemma type_dec_bl X : forall Y, type_beq X Y = true -> X = Y. - Proof. clear base_type_code_lb; pose proof flat_type_dec_bl; induction X, Y; t. Defined. - Lemma type_dec_lb X : forall Y, X = Y -> type_beq X Y = true. - Proof. clear base_type_code_bl; pose proof flat_type_dec_lb; intros; subst Y; induction X; t. Defined. - Definition type_eq_dec (X Y : type) : {X = Y} + {X <> Y} - := match Sumbool.sumbool_of_bool (type_beq X Y) with - | left pf => left (type_dec_bl _ _ pf) - | right pf => right (fun pf' => let pf'' := eq_sym (type_dec_lb _ _ pf') in - Bool.diff_true_false (eq_trans pf'' pf)) - end. - End dec. - Global Coercion Tflat : flat_type >-> type. Infix "*" := Prod : ctype_scope. Notation "A -> B" := (Arrow A B) : ctype_scope. @@ -504,20 +432,10 @@ Global Arguments tuple {_}%type_scope _%ctype_scope _%nat_scope. Global Arguments Prod {_}%type_scope (_ _)%ctype_scope. Global Arguments Arrow {_}%type_scope (_ _)%ctype_scope. Global Arguments Tbase {_}%type_scope _%ctype_scope. +Global Arguments Tflat {_}%type_scope _%ctype_scope. Ltac admit_Wf := apply Wf_admitted. -Global Instance dec_eq_flat_type {base_type_code} `{DecidableRel (@eq base_type_code)} - : DecidableRel (@eq (flat_type base_type_code)). -Proof. - repeat intro; hnf; decide equality; apply dec; auto. -Defined. -Global Instance dec_eq_type {base_type_code} `{DecidableRel (@eq base_type_code)} - : DecidableRel (@eq (type base_type_code)). -Proof. - repeat intro; hnf; decide equality; apply dec; typeclasses eauto. -Defined. - Global Arguments Const {_ _ _ _ _} _. Global Arguments Var {_ _ _ _ _} _. Global Arguments SmartVarf {_ _ _ _ _} _. diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v index a7e2146a6..640db3824 100644 --- a/src/Reflection/TestCase.v +++ b/src/Reflection/TestCase.v @@ -4,6 +4,7 @@ Require Import Crypto.Reflection.Named.Syntax. Require Import Crypto.Reflection.Named.Compile. Require Import Crypto.Reflection.Named.RegisterAssign. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Equality. Require Export Crypto.Reflection.Reify. Require Import Crypto.Reflection.InputSyntax. Require Import Crypto.Reflection.CommonSubexpressionElimination. @@ -81,7 +82,7 @@ Goal True. vm_compute in e. Abort. -Definition example_expr : Syntax.Expr base_type interp_base_type op (Arrow Tnat (Arrow Tnat (Tflat _ tnat))). +Definition example_expr : Syntax.Expr base_type interp_base_type op (Arrow Tnat (Arrow Tnat (Tflat tnat))). Proof. let x := Reify (fun z w => let unused := 1 + 1 in let x := 1 in let y := 1 in (let a := 1 in let '(c, d) := (2, 3) in a + x + (x + x) + (x + x) - (x + x) - a + c + d) + y + z + w)%nat in exact x. @@ -202,7 +203,7 @@ Module bounds. | Prod _ _ => fun x => (constant_bounds _ (fst x), constant_bounds _ (snd x)) end. - Definition example_expr_bounds : Syntax.Expr base_type interp_base_type_bounds op (Arrow Tnat (Arrow Tnat (Tflat _ tnat))) := + Definition example_expr_bounds : Syntax.Expr base_type interp_base_type_bounds op (Arrow Tnat (Arrow Tnat (Tflat tnat))) := Eval vm_compute in (fun var => map base_type op interp_base_type interp_base_type_bounds constant_bounds (fun _ x => x) (fun _ x => x) (example_expr (fun t => var t))). diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v index 466dbd4b5..ea867d024 100644 --- a/src/Reflection/Z/Syntax.v +++ b/src/Reflection/Z/Syntax.v @@ -1,6 +1,7 @@ (** * PHOAS Syntax for expression trees on ℤ *) Require Import Coq.ZArith.ZArith. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Equality. Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations. Require Import Crypto.Util.Equality. Require Import Crypto.Util.ZUtil. diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index d59da1d93..b65c852c0 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -327,8 +327,8 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in + let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in refine (LetIn (UnReturn x) _); let x'' := fresh "x''" in intro x''; diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v index e5fab2a8d..56e4bc47c 100644 --- a/src/SpecificGen/GF2213_32Reflective/Common.v +++ b/src/SpecificGen/GF2213_32Reflective/Common.v @@ -327,8 +327,8 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in + let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in refine (LetIn (UnReturn x) _); let x'' := fresh "x''" in intro x''; diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v index 729c79995..dd7be148a 100644 --- a/src/SpecificGen/GF2519_32Reflective/Common.v +++ b/src/SpecificGen/GF2519_32Reflective/Common.v @@ -327,8 +327,8 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in + let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in refine (LetIn (UnReturn x) _); let x'' := fresh "x''" in intro x''; diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v index aad67f032..644ed7c92 100644 --- a/src/SpecificGen/GF25519_32Reflective/Common.v +++ b/src/SpecificGen/GF25519_32Reflective/Common.v @@ -327,8 +327,8 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in + let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in refine (LetIn (UnReturn x) _); let x'' := fresh "x''" in intro x''; diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v index f639aa0b6..c7b1a69fb 100644 --- a/src/SpecificGen/GF25519_64Reflective/Common.v +++ b/src/SpecificGen/GF25519_64Reflective/Common.v @@ -327,8 +327,8 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in + let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in refine (LetIn (UnReturn x) _); let x'' := fresh "x''" in intro x''; diff --git a/src/SpecificGen/GF41417_32Reflective/Common.v b/src/SpecificGen/GF41417_32Reflective/Common.v index 62d55b463..b9f98cfba 100644 --- a/src/SpecificGen/GF41417_32Reflective/Common.v +++ b/src/SpecificGen/GF41417_32Reflective/Common.v @@ -327,8 +327,8 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in + let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in refine (LetIn (UnReturn x) _); let x'' := fresh "x''" in intro x''; diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v index 977710173..396d2cd35 100644 --- a/src/SpecificGen/GF5211_32Reflective/Common.v +++ b/src/SpecificGen/GF5211_32Reflective/Common.v @@ -327,8 +327,8 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in + let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in refine (LetIn (UnReturn x) _); let x'' := fresh "x''" in intro x''; |