diff options
Diffstat (limited to 'src/Reflection')
-rw-r--r-- | src/Reflection/TestCase.v | 25 | ||||
-rw-r--r-- | src/Reflection/WfReflective.v | 77 | ||||
-rw-r--r-- | src/Reflection/WfReflectiveGen.v | 104 | ||||
-rw-r--r-- | src/Reflection/WfRelReflective.v | 166 | ||||
-rw-r--r-- | src/Reflection/Z/Syntax.v | 50 |
5 files changed, 131 insertions, 291 deletions
diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v index 844fea592..a7e2146a6 100644 --- a/src/Reflection/TestCase.v +++ b/src/Reflection/TestCase.v @@ -96,23 +96,20 @@ Lemma base_type_eq_semidec_is_dec : forall t1 t2, Proof. intros t1 t2; destruct t1, t2; simpl; intros; congruence. Qed. -Definition op_beq t1 tR : op t1 tR -> op t1 tR -> option pointed_Prop - := fun x y => match x, y with - | Add, Add => Some trivial - | Add, _ => None - | Mul, Mul => Some trivial - | Mul, _ => None - | Sub, Sub => Some trivial - | Sub, _ => None - end. +Definition op_beq t1 tR : op t1 tR -> op t1 tR -> reified_Prop + := fun x y => match x, y return bool with + | Add, Add => true + | Add, _ => false + | Mul, Mul => true + | Mul, _ => false + | Sub, Sub => true + | Sub, _ => false + end. Lemma op_beq_bl t1 tR (x y : op t1 tR) - : match op_beq t1 tR x y with - | Some p => to_prop p - | None => False - end -> x = y. + : to_prop (op_beq t1 tR x y) -> x = y. Proof. destruct x; simpl; - refine match y with Add => _ | _ => _ end; tauto. + refine match y with Add => _ | _ => _ end; simpl; tauto. Qed. Ltac reflect_Wf := WfReflective.reflect_Wf base_type_eq_semidec_is_dec op_beq_bl. diff --git a/src/Reflection/WfReflective.v b/src/Reflection/WfReflective.v index d68ed53ac..8a8eef38f 100644 --- a/src/Reflection/WfReflective.v +++ b/src/Reflection/WfReflective.v @@ -45,13 +45,13 @@ - [op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y] for some [op_beq : forall t1 tR, op t1 tR -> op t1 tR - -> option pointed_Prop] *) + -> reified_Prop] *) Require Import Coq.Arith.Arith Coq.Logic.Eqdep_dec. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.WfReflectiveGen. Require Import Crypto.Util.Notations Crypto.Util.Tactics Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Decidable Crypto.Util.ListUtil. -Require Export Crypto.Util.PointedProp. (* export for the [bool >-> option pointed_Prop] coercion *) +Require Export Crypto.Util.PartiallyReifiedProp. (* export for the [bool >-> reified_Prop] coercion *) Require Export Crypto.Util.FixCoqMistakes. @@ -74,8 +74,8 @@ Section language. [pointed_Prop] internally because we need to talk about equality of things of type [var t], for [var : base_type_code -> Type]. It does not hurt to allow extra generality in [op_beq]. *) - Context (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> option pointed_Prop). - Context (op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y). + Context (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> reified_Prop). + Context (op_beq_bl : forall t1 tR x y, to_prop (op_beq t1 tR x y) -> x = y). Context {var1 var2 : base_type_code -> Type}. Local Notation eP := (fun t => var1 (fst t) * var2 (snd t))%type (only parsing). @@ -90,8 +90,8 @@ Section language. Local Notation exprf := (@exprf base_type_code interp_base_type op). Local Notation expr := (@expr base_type_code interp_base_type op). Local Notation duplicate_type := (@duplicate_type base_type_code var1 var2). - Local Notation reflect_wffT := (@reflect_wffT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => eq) op_beq var1 var2). - Local Notation reflect_wfT := (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => eq) op_beq var1 var2). + Local Notation reflect_wffT := (@reflect_wffT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => rEq) op_beq var1 var2). + Local Notation reflect_wfT := (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => rEq) op_beq var1 var2). Local Notation flat_type_eq_semidec_transparent := (@flat_type_eq_semidec_transparent base_type_code base_type_eq_semidec_transparent). Local Notation preflatten_binding_list2 := (@preflatten_binding_list2 base_type_code base_type_eq_semidec_transparent var1 var2). Local Notation type_eq_semidec_transparent := (@type_eq_semidec_transparent base_type_code base_type_eq_semidec_transparent). @@ -105,25 +105,25 @@ Section language. Local Ltac handle_op_beq_correct := repeat match goal with - | [ H : op_beq ?t1 ?tR ?x ?y = _ |- _ ] - => let H' := fresh in - pose proof (op_beq_bl t1 tR x y) as H'; rewrite H in H'; clear H + | [ H : to_prop (op_beq ?t1 ?tR ?x ?y) |- _ ] + => apply op_beq_bl in H end. Local Ltac t_step := match goal with - | _ => progress unfold eq_type_and_var, op_beq', flatten_binding_list2, WfReflectiveGen.preflatten_binding_list2, option_map, and_option_pointed_Prop, eq_semidec_and_gen in * + | [ |- True ] => exact I + | _ => progress cbv beta delta [eq_type_and_var op_beq' flatten_binding_list2 WfReflectiveGen.preflatten_binding_list2 option_map eq_semidec_and_gen] in * | _ => progress simpl in * - | _ => progress break_match - | [ H : interp_flat_type_rel_pointwise2 (fun _ => eq) _ _ |- _ ] - => apply interp_flat_type_rel_pointwise2_eq in H | _ => progress subst + | _ => progress break_innermost_match_step | _ => progress inversion_option - | _ => progress inversion_pointed_Prop + | _ => progress inversion_prod + | _ => progress inversion_reified_Prop | _ => congruence | _ => tauto | _ => progress intros | _ => progress handle_op_beq_correct | _ => progress specialize_by tauto + | [ v : ex _ |- _ ] => destruct v | [ v : sigT _ |- _ ] => destruct v | [ v : prod _ _ |- _ ] => destruct v | [ H : forall x x', _ |- wff (flatten_binding_list _ ?x1 ?x2 ++ _)%list _ _ ] @@ -131,6 +131,7 @@ Section language. | [ H : forall x x', _ |- wf (existT _ _ (?x1, ?x2) :: _)%list _ _ ] => specialize (H x1 x2) | [ H : and _ _ |- _ ] => destruct H + | [ H : to_prop (_ /\ _) |- _ ] => apply to_prop_and_reified_Prop in H; destruct H | [ H : context[duplicate_type (_ ++ _)%list] |- _ ] => rewrite duplicate_type_app in H | [ H : context[List.length (duplicate_type _)] |- _ ] @@ -144,25 +145,28 @@ Section language. | [ H : base_type_eq_semidec_transparent _ _ = None |- False ] => eapply duplicate_type_not_in; eassumption | [ H : List.nth_error _ _ = Some _ |- _ ] => apply List.nth_error_In in H | [ H : List.In _ (duplicate_type _) |- _ ] => eapply duplicate_type_in in H; [ | eassumption.. ] - | [ H : context[match _ with _ => _ end] |- _ ] => revert H; progress break_match + | [ H : context[match _ with _ => _ end] |- _ ] => revert H; progress break_innermost_match | [ |- wff _ _ _ ] => constructor | [ |- wf _ _ _ ] => constructor - | _ => progress unfold and_pointed_Prop in * + | _ => progress unfold and_reified_Prop in * end. Local Ltac t := repeat t_step. Fixpoint reflect_wff (G : list (sigT (fun t => var1 t * var2 t)%type)) {t1 t2 : flat_type} (e1 : @exprf (fun t => nat * var1 t)%type t1) (e2 : @exprf (fun t => nat * var2 t)%type t2) {struct e1} - : match reflect_wffT (duplicate_type G) e1 e2, flat_type_eq_semidec_transparent t1 t2 with - | Some reflective_obligation, Some p + : let reflective_obligation := reflect_wffT (duplicate_type G) e1 e2 in + match flat_type_eq_semidec_transparent t1 t2 with + | Some p => to_prop reflective_obligation -> @wff base_type_code interp_base_type op var1 var2 G t2 (eq_rect _ exprf (unnatize_exprf (List.length G) e1) _ p) (unnatize_exprf (List.length G) e2) - | _, _ => True + | None => True end. Proof. + cbv zeta. destruct e1 as [ | | ? ? ? args | tx ex tC eC | ? ex ? ey ], - e2 as [ | | ? ? ? args' | tx' ex' tC' eC' | ? ex' ? ey' ]; simpl; try solve [ exact I ]; + e2 as [ | | ? ? ? args' | tx' ex' tC' eC' | ? ex' ? ey' ]; simpl; + try solve [ break_match; solve [ exact I | intros [] ] ]; [ clear reflect_wff | clear reflect_wff | specialize (reflect_wff G _ _ args args') @@ -187,11 +191,12 @@ Section language. Fixpoint reflect_wf (G : list (sigT (fun t => var1 t * var2 t)%type)) {t1 t2 : type} (e1 : @expr (fun t => nat * var1 t)%type t1) (e2 : @expr (fun t => nat * var2 t)%type t2) - : match reflect_wfT (duplicate_type G) e1 e2, type_eq_semidec_transparent t1 t2 with - | Some reflective_obligation, Some p + : let reflective_obligation := reflect_wfT (duplicate_type G) e1 e2 in + match type_eq_semidec_transparent t1 t2 with + | Some p => to_prop reflective_obligation -> @wf base_type_code interp_base_type op var1 var2 G t2 (eq_rect _ expr (unnatize_expr (List.length G) e1) _ p) (unnatize_expr (List.length G) e2) - | _, _ => True + | None => True end. Proof. destruct e1 as [ t1 e1 | tx tR f ], @@ -219,15 +224,15 @@ Section Wf. (base_type_eq_semidec_transparent : forall t1 t2 : base_type_code, option (t1 = t2)) (base_type_eq_semidec_is_dec : forall t1 t2, base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2) (op : flat_type base_type_code -> flat_type base_type_code -> Type) - (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> option pointed_Prop) - (op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y) + (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> reified_Prop) + (op_beq_bl : forall t1 tR x y, to_prop (op_beq t1 tR x y) -> x = y) {t : type base_type_code} (e : @Expr base_type_code interp_base_type op t). (** Leads to smaller proofs, but is less generally applicable *) Theorem reflect_Wf_unnatize : (forall var1 var2, - prop_of_option (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => eq) op_beq var1 var2 nil t t (e _) (e _))) + to_prop (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => rEq) op_beq var1 var2 nil t t (e _) (e _))) -> Wf (fun var => unnatize_expr 0 (e (fun t => (nat * var t)%type))). Proof. intros H var1 var2; specialize (H var1 var2). @@ -241,7 +246,7 @@ Section Wf. Theorem reflect_Wf : (forall var1 var2, unnatize_expr 0 (e (fun t => (nat * var1 t)%type)) = e _ - /\ prop_of_option (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => eq) op_beq var1 var2 nil t t (e _) (e _))) + /\ to_prop (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => rEq) op_beq var1 var2 nil t t (e _) (e _))) -> Wf e. Proof. intros H var1 var2. @@ -256,8 +261,22 @@ Ltac generalize_reflect_Wf base_type_eq_semidec_is_dec op_beq_bl := | [ |- @Wf ?base_type_code ?interp_base_type ?op ?t ?e ] => generalize (@reflect_Wf_unnatize base_type_code interp_base_type _ base_type_eq_semidec_is_dec op _ op_beq_bl t e) end. -Ltac use_reflect_Wf := vm_compute; let H := fresh in intro H; apply H; clear H. -Ltac fin_reflect_Wf := repeat constructor. +Ltac use_reflect_Wf := + let H := fresh in + intro H; + lazymatch type of H with + | ?A -> ?B + => cut A + end; + [ abstract vm_cast_no_check H + | clear H ]. +Ltac fin_reflect_Wf := + intros; + lazymatch goal with + | [ |- to_prop ?P ] + => replace P with (trueify P) by abstract vm_cast_no_check (eq_refl P) + end; + apply trueify_true. (** The tactic [reflect_Wf] is the main tactic of this file, used to prove [Syntax.Wf] goals *) Ltac reflect_Wf base_type_eq_semidec_is_dec op_beq_bl := diff --git a/src/Reflection/WfReflectiveGen.v b/src/Reflection/WfReflectiveGen.v index 4935134d8..0d961ec97 100644 --- a/src/Reflection/WfReflectiveGen.v +++ b/src/Reflection/WfReflectiveGen.v @@ -50,7 +50,7 @@ Require Import Coq.Arith.Arith Coq.Logic.Eqdep_dec. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Util.Notations Crypto.Util.Tactics Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Decidable Crypto.Util.ListUtil. -Require Export Crypto.Util.PointedProp. (* export for the [bool >-> option pointed_Prop] coercion *) +Require Export Crypto.Util.PartiallyReifiedProp. (* export for the [bool >-> reified_Prop] coercion *) Require Export Crypto.Util.FixCoqMistakes. @@ -67,15 +67,15 @@ Section language. (base_type_eq_semidec_transparent : forall t1 t2 : base_type_code, option (t1 = t2)) (base_type_eq_semidec_is_dec : forall t1 t2, base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2) (op : flat_type base_type_code -> flat_type base_type_code -> Type) - (R : forall t, interp_base_type1 t -> interp_base_type2 t -> Prop). + (R : forall t, interp_flat_type interp_base_type1 t -> interp_flat_type interp_base_type2 t -> reified_Prop). (** In practice, semi-deciding equality of operators should either return [Some trivial] or [None], and not make use of the generality of [pointed_Prop]. However, we need to use [pointed_Prop] internally because we need to talk about equality of things of type [var t], for [var : base_type_code -> Type]. It does not hurt to allow extra generality in [op_beq]. *) - Context (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> option pointed_Prop). - Context (op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y). + Context (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> reified_Prop). + Context (op_beq_bl : forall t1 tR x y, to_prop (op_beq t1 tR x y) -> x = y). Context {var1 var2 : base_type_code -> Type}. Local Notation eP := (fun t => var1 (fst t) * var2 (snd t))%type (only parsing). @@ -151,13 +151,13 @@ Section language. { rewrite base_type_eq_semidec_transparent_refl; rewrite_hyp !*; reflexivity. } Qed. - Definition op_beq' t1 tR t1' tR' (x : op t1 tR) (y : op t1' tR') : option pointed_Prop + Definition op_beq' t1 tR t1' tR' (x : op t1 tR) (y : op t1' tR') : reified_Prop := match flat_type_eq_semidec_transparent t1 t1', flat_type_eq_semidec_transparent tR tR' with | Some p, Some q => match p in (_ = t1'), q in (_ = tR') return op t1' tR' -> _ with | eq_refl, eq_refl => fun y => op_beq _ _ x y end y - | _, _ => None + | _, _ => rFalse end. (** While [Syntax.wff] is parameterized over a list of [sigT (fun t @@ -178,27 +178,27 @@ Section language. about [Syntax.wff] itself. *) Definition eq_semidec_and_gen {T} (semidec : forall x y : T, option (x = y)) - (t t' : T) (f g : T -> Type) (R : forall t, f t -> g t -> Prop) + (t t' : T) (f g : T -> Type) (R : forall t, f t -> g t -> reified_Prop) (x : f t) (x' : g t') - : option pointed_Prop + : reified_Prop := match semidec t t' with | Some p - => Some (inject (R _ (eq_rect _ f x _ p) x')) - | None => None + => R _ (eq_rect _ f x _ p) x' + | None => rFalse end. (* Here is where we use the generality of [pointed_Prop], to say that two things of type [var1] are equal, and two things of type [var2] are equal. *) - Definition eq_type_and_var : sigT eP -> sigT eP -> option pointed_Prop + Definition eq_type_and_var : sigT eP -> sigT eP -> reified_Prop := fun x y => (eq_semidec_and_gen - base_type_eq_semidec_transparent _ _ var1 var1 (fun _ => eq) (fst (projT2 x)) (fst (projT2 y)) + base_type_eq_semidec_transparent _ _ var1 var1 (fun _ => rEq) (fst (projT2 x)) (fst (projT2 y)) /\ eq_semidec_and_gen - base_type_eq_semidec_transparent _ _ var2 var2 (fun _ => eq) (snd (projT2 x)) (snd (projT2 y)))%option_pointed_prop. + base_type_eq_semidec_transparent _ _ var2 var2 (fun _ => rEq) (snd (projT2 x)) (snd (projT2 y)))%reified_prop. Definition rel_type_and_const (t t' : flat_type) (x : interp_flat_type1 t) (y : interp_flat_type2 t') - : option pointed_Prop + : reified_Prop := eq_semidec_and_gen - flat_type_eq_semidec_transparent _ _ interp_flat_type1 interp_flat_type2 (fun t => interp_flat_type_rel_pointwise2 R) x y. + flat_type_eq_semidec_transparent _ _ interp_flat_type1 interp_flat_type2 R x y. Definition duplicate_type (ls : list (sigT (fun t => var1 t * var2 t)%type)) : list (sigT eP) := List.map (fun v => existT eP (projT1 v, projT1 v) (projT2 v)) ls. @@ -292,71 +292,61 @@ Section language. (e1 : @exprf1 (fun t => nat * var1 t)%type t1) (e2 : @exprf2 (fun t => nat * var2 t)%type t2) {struct e1} - : option pointed_Prop - := match e1, e2 return option _ with + : reified_Prop + := match e1, e2 with | Const t0 x, Const t1 y => match flat_type_eq_semidec_transparent t0 t1 with - | Some p => Some (inject (interp_flat_type_rel_pointwise2 R (eq_rect _ interp_flat_type1 x _ p) y)) - | None => None + | Some p => R _ (eq_rect _ interp_flat_type1 x _ p) y + | None => rFalse end - | Const _ _, _ => None + | Const _ _, _ => rFalse | Var t0 x, Var t1 y => match beq_nat (fst x) (fst y), List.nth_error G (List.length G - S (fst x)) with | true, Some v => eq_type_and_var v (existT _ (t0, t1) (snd x, snd y)) - | _, _ => None + | _, _ => rFalse end - | Var _ _, _ => None + | Var _ _, _ => rFalse | Op t1 tR op args, Op t1' tR' op' args' - => match @reflect_wffT G t1 t1' args args', op_beq' t1 tR t1' tR' op op' with - | Some p, Some q => Some (p /\ q)%pointed_prop - | _, _ => None - end - | Op _ _ _ _, _ => None + => (@reflect_wffT G t1 t1' args args' /\ op_beq' t1 tR t1' tR' op op')%reified_prop + | Op _ _ _ _, _ => rFalse | LetIn tx ex tC eC, LetIn tx' ex' tC' eC' - => match @reflect_wffT G tx tx' ex ex', @flatten_binding_list2 tx tx', flat_type_eq_semidec_transparent tC tC' with - | Some p, Some G0, Some _ - => Some (p /\ inject (forall (x : interp_flat_type var1 tx) (x' : interp_flat_type var2 tx'), - match @reflect_wffT (G0 x x' ++ G)%list _ _ - (eC (snd (natize_interp_flat_type (List.length G) x))) - (eC' (snd (natize_interp_flat_type (List.length G) x'))) with - | Some p => to_prop p - | None => False - end)) - | _, _, _ => None + => let p := @reflect_wffT G tx tx' ex ex' in + match @flatten_binding_list2 tx tx', flat_type_eq_semidec_transparent tC tC' with + | Some G0, Some _ + => p + /\ (∀ (x : interp_flat_type var1 tx) (x' : interp_flat_type var2 tx'), + @reflect_wffT (G0 x x' ++ G)%list _ _ + (eC (snd (natize_interp_flat_type (List.length G) x))) + (eC' (snd (natize_interp_flat_type (List.length G) x')))) + | _, _ => rFalse end - | LetIn _ _ _ _, _ => None + | LetIn _ _ _ _, _ => rFalse | Pair tx ex ty ey, Pair tx' ex' ty' ey' - => match @reflect_wffT G tx tx' ex ex', @reflect_wffT G ty ty' ey ey' with - | Some p, Some q => Some (p /\ q) - | _, _ => None - end - | Pair _ _ _ _, _ => None - end%pointed_prop. + => @reflect_wffT G tx tx' ex ex' /\ @reflect_wffT G ty ty' ey ey' + | Pair _ _ _ _, _ => rFalse + end%reified_prop. Fixpoint reflect_wfT (G : list (sigT (fun t => var1 (fst t) * var2 (snd t))%type)) {t1 t2 : type} (e1 : @expr1 (fun t => nat * var1 t)%type t1) (e2 : @expr2 (fun t => nat * var2 t)%type t2) {struct e1} - : option pointed_Prop - := match e1, e2 return option _ with + : reified_Prop + := match e1, e2 with | Return _ x, Return _ y => reflect_wffT G x y - | Return _ _, _ => None + | Return _ _, _ => rFalse | Abs tx tR f, Abs tx' tR' f' => match @flatten_binding_list2 tx tx', type_eq_semidec_transparent tR tR' with | Some G0, Some _ - => Some (inject (forall (x : interp_flat_type var1 tx) (x' : interp_flat_type var2 tx'), - match @reflect_wfT (G0 x x' ++ G)%list _ _ - (f (snd (natize_interp_flat_type (List.length G) x))) - (f' (snd (natize_interp_flat_type (List.length G) x'))) with - | Some p => to_prop p - | None => False - end)) - | _, _ => None + => ∀ (x : interp_flat_type var1 tx) (x' : interp_flat_type var2 tx'), + @reflect_wfT (G0 x x' ++ G)%list _ _ + (f (snd (natize_interp_flat_type (List.length G) x))) + (f' (snd (natize_interp_flat_type (List.length G) x'))) + | _, _ => rFalse end - | Abs _ _ _, _ => None - end%pointed_prop. + | Abs _ _ _, _ => rFalse + end%reified_prop. End language. Global Arguments reflect_wffT {_ _ _} _ {op} R _ {var1 var2} G {t1 t2} _ _. diff --git a/src/Reflection/WfRelReflective.v b/src/Reflection/WfRelReflective.v deleted file mode 100644 index 0135f6afb..000000000 --- a/src/Reflection/WfRelReflective.v +++ /dev/null @@ -1,166 +0,0 @@ -(** * A reflective Version of [WfRel] proofs *) -(** See [WfReflective.v] and [WfReflectiveGen.v] for comments. *) -Require Import Coq.Arith.Arith Coq.Logic.Eqdep_dec. -Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.WfRel. -Require Import Crypto.Reflection.WfReflectiveGen. -Require Import Crypto.Util.Notations Crypto.Util.Tactics Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Decidable Crypto.Util.ListUtil. -Require Export Crypto.Util.PointedProp. (* export for the [bool >-> option pointed_Prop] coercion *) -Require Export Crypto.Util.FixCoqMistakes. - - -Section language. - (** To be able to optimize away so much of the [Syntax.wff] proof, - we must be able to decide a few things: equality of base types, - and equality of operator codes. Since we will be casting across - the equality proofs of base types, we require that this - semi-decider give transparent proofs. (This requirement is not - enforced, but it will block [vm_compute] when trying to use the - lemma in this file.) *) - Context (base_type_code : Type). - Context (interp_base_type1 interp_base_type2 : base_type_code -> Type). - Context (base_type_eq_semidec_transparent : forall t1 t2 : base_type_code, option (t1 = t2)). - Context (base_type_eq_semidec_is_dec : forall t1 t2, base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2). - Context (op : flat_type base_type_code -> flat_type base_type_code -> Type). - Context (R : forall t, interp_base_type1 t -> interp_base_type2 t -> Prop). - (** In practice, semi-deciding equality of operators should either - return [Some trivial] or [None], and not make use of the - generality of [pointed_Prop]. However, we need to use - [pointed_Prop] internally because we need to talk about equality - of things of type [var t], for [var : base_type_code -> Type]. - It does not hurt to allow extra generality in [op_beq]. *) - Context (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> option pointed_Prop). - Context (op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y). - Context {var1 var2 : base_type_code -> Type}. - - Local Notation eP := (fun t => var1 (fst t) * var2 (snd t))%type (only parsing). - - (* convenience notations that fill in some arguments used across the section *) - Local Notation flat_type := (flat_type base_type_code). - Local Notation type := (type base_type_code). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Local Notation interp_type1 := (interp_type interp_base_type1). - Local Notation interp_type2 := (interp_type interp_base_type2). - Local Notation interp_flat_type1 := (interp_flat_type interp_base_type1). - Local Notation interp_flat_type2 := (interp_flat_type interp_base_type2). - Local Notation exprf1 := (@exprf base_type_code interp_base_type1 op). - Local Notation exprf2 := (@exprf base_type_code interp_base_type2 op). - Local Notation expr1 := (@expr base_type_code interp_base_type1 op). - Local Notation expr2 := (@expr base_type_code interp_base_type2 op). - Local Notation duplicate_type := (@duplicate_type base_type_code var1 var2). - Local Notation reflect_wffT := (@reflect_wffT base_type_code interp_base_type1 interp_base_type2 base_type_eq_semidec_transparent op R op_beq var1 var2). - Local Notation reflect_wfT := (@reflect_wfT base_type_code interp_base_type1 interp_base_type2 base_type_eq_semidec_transparent op R op_beq var1 var2). - Local Notation flat_type_eq_semidec_transparent := (@flat_type_eq_semidec_transparent base_type_code base_type_eq_semidec_transparent). - Local Notation preflatten_binding_list2 := (@preflatten_binding_list2 base_type_code base_type_eq_semidec_transparent var1 var2). - Local Notation type_eq_semidec_transparent := (@type_eq_semidec_transparent base_type_code base_type_eq_semidec_transparent). - - Local Ltac handle_op_beq_correct := - repeat match goal with - | [ H : op_beq ?t1 ?tR ?x ?y = _ |- _ ] - => let H' := fresh in - pose proof (op_beq_bl t1 tR x y) as H'; rewrite H in H'; clear H - end. - Local Ltac t_step := - match goal with - | _ => progress unfold eq_type_and_var, op_beq', flatten_binding_list2, WfReflectiveGen.preflatten_binding_list2, option_map, and_option_pointed_Prop, eq_semidec_and_gen in * - | _ => progress simpl in * - | _ => progress break_match - | _ => progress subst - | _ => progress inversion_option - | _ => progress inversion_pointed_Prop - | _ => congruence - | _ => tauto - | _ => progress intros - | _ => progress handle_op_beq_correct - | _ => progress specialize_by tauto - | [ v : sigT _ |- _ ] => destruct v - | [ v : prod _ _ |- _ ] => destruct v - | [ H : forall x x', _ |- rel_wff _ (flatten_binding_list _ ?x1 ?x2 ++ _)%list _ _ ] - => specialize (H x1 x2) - | [ H : forall x x', _ |- rel_wf _ (existT _ _ (?x1, ?x2) :: _)%list _ _ ] - => specialize (H x1 x2) - | [ H : and _ _ |- _ ] => destruct H - | [ H : context[duplicate_type (_ ++ _)%list] |- _ ] - => rewrite duplicate_type_app in H - | [ H : context[List.length (duplicate_type _)] |- _ ] - => rewrite duplicate_type_length in H - | [ H : context[List.length (_ ++ _)%list] |- _ ] - => rewrite List.app_length in H - | [ |- rel_wff _ _ (unnatize_exprf (fst _) _) (unnatize_exprf (fst _) _) ] - => erewrite length_natize_interp_flat_type1, length_natize_interp_flat_type2; eassumption - | [ |- rel_wf _ _ (unnatize_exprf (fst _) _) (unnatize_exprf (fst _) _) ] - => erewrite length_natize_interp_flat_type1, length_natize_interp_flat_type2; eassumption - | [ H : base_type_eq_semidec_transparent _ _ = None |- False ] => eapply duplicate_type_not_in; eassumption - | [ H : List.nth_error _ _ = Some _ |- _ ] => apply List.nth_error_In in H - | [ H : List.In _ (duplicate_type _) |- _ ] => eapply duplicate_type_in in H; [ | eassumption.. ] - | [ H : context[match _ with _ => _ end] |- _ ] => revert H; progress break_match - | [ |- rel_wff _ _ _ _ ] => constructor - | [ |- rel_wf _ _ _ _ ] => constructor - | _ => progress unfold and_pointed_Prop in * - end. - Local Ltac t := repeat t_step. - Fixpoint reflect_rel_wff (G : list (sigT (fun t => var1 t * var2 t)%type)) - {t1 t2 : flat_type} - (e1 : @exprf1 (fun t => nat * var1 t)%type t1) - (e2 : @exprf2 (fun t => nat * var2 t)%type t2) - {struct e1} - : match reflect_wffT (duplicate_type G) e1 e2, flat_type_eq_semidec_transparent t1 t2 with - | Some reflective_obligation, Some p - => to_prop reflective_obligation - -> @rel_wff base_type_code interp_base_type1 interp_base_type2 op R var1 var2 G t2 (eq_rect _ exprf1 (unnatize_exprf (List.length G) e1) _ p) (unnatize_exprf (List.length G) e2) - | _, _ => True - end. - Proof. - destruct e1 as [ | | ? ? ? args | tx ex tC eC | ? ex ? ey ], - e2 as [ | | ? ? ? args' | tx' ex' tC' eC' | ? ex' ? ey' ]; simpl; try solve [ exact I ]; - [ clear reflect_rel_wff - | clear reflect_rel_wff - | specialize (reflect_rel_wff G _ _ args args') - | pose proof (reflect_rel_wff G _ _ ex ex'); - pose proof (fun x x' - => match preflatten_binding_list2 tx tx' as v return match v with Some _ => _ | None => True end with - | Some G0 - => reflect_rel_wff - (G0 x x' ++ G)%list _ _ - (eC (snd (natize_interp_flat_type (length (duplicate_type G)) x))) - (eC' (snd (natize_interp_flat_type (length (duplicate_type G)) x'))) - | None => I - end); - clear reflect_rel_wff - | pose proof (reflect_rel_wff G _ _ ex ex'); pose proof (reflect_rel_wff G _ _ ey ey'); clear reflect_rel_wff ]. - { t. } - { t. } - { t. } - { t. } - { t. } - Qed. - Fixpoint reflect_rel_wf (G : list (sigT (fun t => var1 t * var2 t)%type)) - {t1 t2 : type} - (e1 : @expr1 (fun t => nat * var1 t)%type t1) - (e2 : @expr2 (fun t => nat * var2 t)%type t2) - : match reflect_wfT (duplicate_type G) e1 e2, type_eq_semidec_transparent t1 t2 with - | Some reflective_obligation, Some p - => to_prop reflective_obligation - -> @rel_wf base_type_code interp_base_type1 interp_base_type2 op R var1 var2 G t2 (eq_rect _ expr1 (unnatize_expr (List.length G) e1) _ p) (unnatize_expr (List.length G) e2) - | _, _ => True - end. - Proof. - destruct e1 as [ t1 e1 | tx tR f ], - e2 as [ t2 e2 | tx' tR' f' ]; simpl; try solve [ exact I ]; - [ clear reflect_rel_wf; - pose proof (@reflect_rel_wff G t1 t2 e1 e2) - | pose proof (fun x x' - => match preflatten_binding_list2 tx tx' as v return match v with Some _ => _ | None => True end with - | Some G0 - => reflect_rel_wf - (G0 x x' ++ G)%list _ _ - (f (snd (natize_interp_flat_type (length (duplicate_type G)) x))) - (f' (snd (natize_interp_flat_type (length (duplicate_type G)) x'))) - | None => I - end); - clear reflect_rel_wf ]. - { t. } - { t. } - Qed. -End language. diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v index 2d31ec8e2..4b23cc274 100644 --- a/src/Reflection/Z/Syntax.v +++ b/src/Reflection/Z/Syntax.v @@ -4,7 +4,7 @@ Require Import Crypto.Reflection.Syntax. Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations. Require Import Crypto.Util.Equality. Require Import Crypto.Util.ZUtil. -Require Import Crypto.Util.PointedProp. +Require Import Crypto.Util.PartiallyReifiedProp. Export Syntax.Notations. Local Set Boolean Equality Schemes. @@ -57,31 +57,31 @@ Proof. unfold base_type_eq_semidec_transparent; congruence. Qed. -Definition op_beq t1 tR (f g : op t1 tR) : option pointed_Prop - := option_pointed_Prop_of_bool match f, g with - | Add, Add => true - | Add, _ => false - | Sub, Sub => true - | Sub, _ => false - | Mul, Mul => true - | Mul, _ => false - | Shl, Shl => true - | Shl, _ => false - | Shr, Shr => true - | Shr, _ => false - | Land, Land => true - | Land, _ => false - | Lor, Lor => true - | Lor, _ => false - | Neg, Neg => true - | Neg, _ => false - | Cmovne, Cmovne => true - | Cmovne, _ => false - | Cmovle, Cmovle => true - | Cmovle, _ => false - end. +Definition op_beq t1 tR (f g : op t1 tR) : reified_Prop + := match f, g return bool with + | Add, Add => true + | Add, _ => false + | Sub, Sub => true + | Sub, _ => false + | Mul, Mul => true + | Mul, _ => false + | Shl, Shl => true + | Shl, _ => false + | Shr, Shr => true + | Shr, _ => false + | Land, Land => true + | Land, _ => false + | Lor, Lor => true + | Lor, _ => false + | Neg, Neg => true + | Neg, _ => false + | Cmovne, Cmovne => true + | Cmovne, _ => false + | Cmovle, Cmovle => true + | Cmovle, _ => false + end. -Lemma op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y. +Lemma op_beq_bl : forall t1 tR x y, to_prop (op_beq t1 tR x y) -> x = y. Proof. intros ?? x; destruct x; intro y; |