From 20d1a5816a33568f2fe13e28445396c476a49d27 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Mar 2017 18:54:55 -0400 Subject: Finish proof of wf_map_cast After | File Name | Before || Change --------------------------------------------------------------------- 0m20.75s | Total | 0m15.19s || +0m05.56s --------------------------------------------------------------------- 0m19.33s | Reflection/Named/MapCastWf | 0m13.82s || +0m05.50s 0m00.79s | Reflection/MapCastByDeBruijnInterp | 0m00.75s || +0m00.04s 0m00.64s | Reflection/MapCastByDeBruijnWf | 0m00.62s || +0m00.02s --- src/Reflection/MapCastByDeBruijnInterp.v | 2 +- src/Reflection/MapCastByDeBruijnWf.v | 7 +- src/Reflection/Named/MapCastWf.v | 130 +++++++++++++++++++++---------- 3 files changed, 94 insertions(+), 45 deletions(-) (limited to 'src/Reflection') diff --git a/src/Reflection/MapCastByDeBruijnInterp.v b/src/Reflection/MapCastByDeBruijnInterp.v index add7014ce..0e425886b 100644 --- a/src/Reflection/MapCastByDeBruijnInterp.v +++ b/src/Reflection/MapCastByDeBruijnInterp.v @@ -106,7 +106,7 @@ Section language. { erewrite (interp_compile (ContextOk:=PositiveContextOk)), interp_linearize; [ reflexivity | apply wf_linearize; auto | .. | eassumption ]; auto using name_list_unique_DefaultNamesFor. } - { intro; eapply wf_map_cast with (t := Arrow _ _) (oldValues := empty); eauto using PositiveContextOk with typeclass_instances. + { intro; eapply wf_map_cast with (t := Arrow _ _) (fValues := empty); eauto using PositiveContextOk with typeclass_instances. { eapply (wf_compile (ContextOk:=PositiveContextOk)); [ apply wf_linearize; auto | .. | eassumption ]. auto using name_list_unique_DefaultNamesFor. } diff --git a/src/Reflection/MapCastByDeBruijnWf.v b/src/Reflection/MapCastByDeBruijnWf.v index b4edb51c8..c5fbfa695 100644 --- a/src/Reflection/MapCastByDeBruijnWf.v +++ b/src/Reflection/MapCastByDeBruijnWf.v @@ -67,7 +67,7 @@ Section language. abstract (intro; erewrite base_type_code_lb in pf by eassumption; congruence). } Defined. - Lemma MapCastCorrect + Lemma Wf_MapCast {t} (e : Expr base_type_code op t) (Hwf : Wf e) (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) @@ -84,11 +84,10 @@ Section language. (PositiveContext base_type_code _ base_type_code_beq base_type_code_bl_transparent) PositiveContextOk PositiveContextOk (failb _) (failb _) _ e1); - (eapply wf_map_cast with (oldValues:=empty); eauto using PositiveContextOk with typeclass_instances); + (eapply wf_map_cast with (fValues:=empty); eauto using PositiveContextOk with typeclass_instances); try (eapply (wf_compile (ContextOk:=PositiveContextOk)); [ apply wf_linearize; eauto | .. | eassumption ]); try solve [ auto using name_list_unique_DefaultNamesFor | intros ???; rewrite lookupb_empty by apply PositiveContextOk; congruence ]. - (* XXX why do we need cast_backb for arbitrary var ? *) - Abort. + Qed. End language. diff --git a/src/Reflection/Named/MapCastWf.v b/src/Reflection/Named/MapCastWf.v index d5015a87c..a3196dbcc 100644 --- a/src/Reflection/Named/MapCastWf.v +++ b/src/Reflection/Named/MapCastWf.v @@ -13,6 +13,7 @@ Require Import Crypto.Util.PointedProp. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Bool. Require Import Crypto.Util.Option. +Require Import Crypto.Util.Prod. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.Tactics.BreakMatch. @@ -35,10 +36,9 @@ Section language. {interp_base_type : base_type_code -> Type} (interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst) - (cast_backb: forall t b, interp_base_type (pick_typeb t b) -> interp_base_type t). - Let cast_back : forall t b, interp_flat_type interp_base_type (@pick_type t b) -> interp_flat_type interp_base_type t - := fun t b => SmartFlatTypeMapUnInterp cast_backb. - Context {Context : Context Name interp_base_type} + {FullContext : Context Name (fun t => { b : interp_base_type_bounds t & interp_base_type (pick_typeb t b) }%type)} + (FullContextOk : ContextOk FullContext) + {Context : Context Name interp_base_type} (ContextOk : ContextOk Context) (base_type_dec : DecidableRel (@eq base_type_code)) (Name_dec : DecidableRel (@eq Name)). @@ -66,6 +66,7 @@ Section language. | _ => progress unfold option_map in * end. + Local Ltac handle_lookupb_step_extra := fail. Local Ltac handle_lookupb_step := let do_eq_dec dec t t' := first [ constr_eq t t'; fail 1 @@ -101,6 +102,7 @@ Section language. => rewrite find_Name_SmartFlatTypeMapInterp2 with (base_type_code_dec:=base_type_dec) in H | [ H : find_Name_and_val _ _ _ _ _ _ _ = None |- _ ] => apply find_Name_and_val_None_iff in H + | _ => progress handle_lookupb_step_extra (* destructers *) | [ |- context[find_Name_and_val ?tdec ?ndec ?t ?n ?N ?V ?default] ] => destruct (find_Name_and_val tdec ndec t n N V default) eqn:? @@ -131,10 +133,16 @@ Section language. match goal with | [ H : ?T, H' : ?T |- _ ] => clear H | [ H : forall x, Some _ = Some x -> _ |- _ ] => specialize (H _ eq_refl) + | [ H : ?x = Some _, IH : forall a b c, ?x = Some _ -> _ |- _ ] + => specialize (IH _ _ _ H) | [ H : ?x = Some _, IH : forall a b, ?x = Some _ -> _ |- _ ] => specialize (IH _ _ H) | [ H : ?x = Some _, IH : forall a, ?x = Some _ -> _ |- _ ] => specialize (IH _ H) + | [ H : forall t n x y z, lookupb ?ctx n = _ -> _, H' : lookupb ?ctx ?n' = _ |- _ ] + => specialize (H _ _ _ _ _ H') + | [ H : forall t n x y, lookupb ?ctx n = _ -> _, H' : lookupb ?ctx ?n' = _ |- _ ] + => specialize (H _ _ _ _ H') | [ H : forall t n v, lookupb ?ctx n = _ -> _, H' : lookupb ?ctx ?n' = _ |- _ ] => specialize (H _ _ _ H') | _ => progress specialize_by auto @@ -145,34 +153,50 @@ Section language. | progress destruct_head'_ex | progress destruct_head'_and | progress inversion_option + | progress inversion_prod | progress inversion_sigma | progress autorewrite with push_prop_of_option in * | progress break_match_hyps ]. - Local Ltac do_specialize_IHe := - repeat match goal with - | [ IH : context[mapf_cast _ ?e], H' : mapf_cast ?ctx ?e = _ |- _ ] - => let check_tac _ := (rewrite H' in IH) in - first [ specialize (IH ctx); check_tac () - | specialize (fun a => IH a ctx); check_tac () - | specialize (fun a b => IH a b ctx); check_tac () ] - | [ H : forall x y z w, Some _ = Some _ -> _ |- _ ] - => first [ specialize (H _ _ _ _ eq_refl) - | specialize (fun x y => H x y _ _ eq_refl) ] - | [ H : forall x y z, Some _ = Some _ -> _ |- _ ] - => first [ specialize (H _ _ _ eq_refl) - | specialize (fun x => H x _ _ eq_refl) ] - | [ H : forall x y, Some _ = Some _ -> _ |- _ ] - => first [ specialize (H _ _ eq_refl) - | specialize (fun x => H x _ eq_refl) ] - | _ => progress specialize_by_assumption - | [ H : forall a b, prop_of_option (Named.wff a ?e) -> _, H' : prop_of_option (Named.wff _ ?e) |- _ ] - => specialize (fun b => H _ b H') - | [ H : forall a b, prop_of_option (Named.wff a ?e) -> _, H' : forall v, prop_of_option (Named.wff _ ?e) |- _ ] - => specialize (fun b v => H _ b (H' v)) - | [ H : forall b v, _ -> prop_of_option (Named.wff b ?e) |- prop_of_option (Named.wff ?ctx ?e) ] - => specialize (H ctx) - end. + Local Ltac do_specialize_IHe_step := + match goal with + | [ IH : context[mapf_cast _ ?e], H' : mapf_cast ?ctx ?e = _ |- _ ] + => let check_tac _ := (rewrite H' in IH) in + first [ specialize (IH ctx); check_tac () + | specialize (fun a => IH a ctx); check_tac () + | specialize (fun a b => IH a b ctx); check_tac () ] + | [ H : forall x y z w, Some _ = Some _ -> _ |- _ ] + => first [ specialize (H _ _ _ _ eq_refl) + | specialize (fun x y => H x y _ _ eq_refl) ] + | [ H : forall x y z, Some _ = Some _ -> _ |- _ ] + => first [ specialize (H _ _ _ eq_refl) + | specialize (fun x => H x _ _ eq_refl) ] + | [ H : forall x y, Some _ = Some _ -> _ |- _ ] + => first [ specialize (H _ _ eq_refl) + | specialize (fun x => H x _ eq_refl) ] + | _ => progress specialize_by_assumption + | [ H : forall a b, prop_of_option (Named.wff a ?e) -> _, H' : prop_of_option (Named.wff _ ?e) |- _ ] + => specialize (fun b => H _ b H') + | [ H : forall b v, _ -> prop_of_option (Named.wff b ?e) |- prop_of_option (Named.wff ?ctx ?e) ] + => specialize (H ctx) + | [ H : forall b v, _ -> _ -> prop_of_option (Named.wff b ?e) |- prop_of_option (Named.wff ?ctx ?e) ] + => specialize (H ctx) + | [ H : forall a b, _ -> _ -> _ -> prop_of_option (Named.wff b ?e) |- prop_of_option (Named.wff ?ctx ?e) ] + => specialize (fun a => H a ctx) + | [ H : forall a b, prop_of_option (Named.wff a ?e) -> _, H' : forall v, prop_of_option (Named.wff _ ?e) |- _ ] + => specialize (fun b v => H _ b (H' v)) + end. + Ltac do_specialize_IHe := repeat do_specialize_IHe_step. + + Definition make_fContext_value {t} {b : interp_flat_type interp_base_type_bounds t} + (v : interp_flat_type interp_base_type (pick_type t b)) + : interp_flat_type + (fun t => { b : interp_base_type_bounds t & interp_base_type (pick_typeb t b)}) + t + := SmartFlatTypeMapUnInterp2 + (fun t b (v : interp_flat_type _ (Tbase _)) + => existT (fun b => interp_base_type (pick_typeb t b)) b v) + v. Local Ltac t_step := first [ progress intros @@ -186,23 +210,49 @@ Section language. | progress do_specialize_IHe | match goal with | [ IH : forall v, _ -> ?T, v' : interp_flat_type _ _ |- ?T ] - => apply (IH (cast_back _ _ v')); clear IH + => apply (IH (make_fContext_value v')); clear IH end ]. Local Ltac t := repeat t_step. + Lemma find_Name_and_val_make_fContext_value_Some {T} + {N : interp_flat_type (fun _ : base_type_code => Name) T} + {B : interp_flat_type interp_base_type_bounds T} + {V : interp_flat_type interp_base_type (pick_type T B)} + {n : Name} + {t : base_type_code} + {v : { b : interp_base_type_bounds t & interp_base_type (pick_typeb t b)}} + {b} + (Hn : find_Name Name_dec n N = Some t) + (Hf : find_Name_and_val base_type_dec Name_dec t n N (make_fContext_value V) None = Some v) + (Hb : find_Name_and_val base_type_dec Name_dec t n N B None = Some b) + (N' := SmartFlatTypeMapInterp2 (var'':=fun _ => Name) (f:=pick_typeb) (fun _ _ n => n) _ N) + : b = projT1 v /\ find_Name_and_val base_type_dec Name_dec (pick_typeb t (projT1 v)) n N' V None = Some (projT2 v). + Proof. + eapply (find_Name_and_val_SmartFlatTypeMapUnInterp2_Some_Some base_type_dec Name_dec (h:=@projT1 _ _) (i:=@projT2 _ _) (f:=pick_typeb) (g:=fun _ => existT _)); + auto. + Qed. + + Local Ltac handle_lookupb_step_extra ::= + lazymatch goal with + | [ H : find_Name _ ?n ?N = Some ?t, + H' : find_Name_and_val _ _ ?t ?n ?N (@make_fContext_value ?T ?B ?v) None = Some ?v', + H'' : find_Name_and_val _ _ ?t ?n ?N ?B None = Some _ + |- _ ] + => pose proof (find_Name_and_val_make_fContext_value_Some H H' H''); clear H' + end. Lemma wff_mapf_cast {t} (e:exprf base_type_code op Name t) : forall - (oldValues:Context) + (fValues:FullContext) (newValues:Context) (varBounds:BoundsContext) {b} e' (He':mapf_cast varBounds e = Some (existT _ b e')) - (Hwf : prop_of_option (Named.wff oldValues e)) + (Hwf : prop_of_option (Named.wff fValues e)) (Hctx:forall {t} n v, - lookupb (t:=t) oldValues n = Some v - -> exists b, lookupb (t:=t) varBounds n = Some b - /\ exists v', lookupb (t:=pick_typeb t b) newValues n = Some v'), + lookupb (t:=t) fValues n = Some v + -> lookupb (t:=t) varBounds n = Some (projT1 v) + /\ lookupb (t:=pick_typeb t (projT1 v)) newValues n = Some (projT2 v)), prop_of_option (Named.wff newValues e'). Proof. induction e; t. Qed. @@ -210,15 +260,15 @@ Section language. {t} (e:expr base_type_code op Name t) (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) : forall - (oldValues:Context) + (fValues:FullContext) (newValues:Context) (varBounds:BoundsContext) {b} e' (He':map_cast varBounds e input_bounds = Some (existT _ b e')) - (Hwf : Named.wf oldValues e) + (Hwf : Named.wf fValues e) (Hctx:forall {t} n v, - lookupb (t:=t) oldValues n = Some v - -> exists b, lookupb (t:=t) varBounds n = Some b - /\ exists v', lookupb (t:=pick_typeb t b) newValues n = Some v'), + lookupb (t:=t) fValues n = Some v + -> lookupb (t:=t) varBounds n = Some (projT1 v) + /\ lookupb (t:=pick_typeb t (projT1 v)) newValues n = Some (projT2 v)), Named.wf newValues e'. Proof. unfold Named.wf, map_cast, option_map, interp; simpl; intros. @@ -228,7 +278,7 @@ Section language. | progress break_match_hyps | progress destruct_head' sigT | progress simpl in * ]. - match goal with v : _ |- _ => specialize (Hwf (cast_back _ _ v)) end. + match goal with v : _ |- _ => specialize (Hwf (make_fContext_value v)) end. eapply wff_mapf_cast; eauto; []. t. Qed. -- cgit v1.2.3