From d3054c8ba755bea855cbcecd12b1e54529d15693 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 15 May 2017 16:00:45 -0400 Subject: Add Wf_from_unit This one is much easier to compute with, and it means we can get rid of a lot of pesky Named.wff proofs. --- src/Compilers/Named/Wf.v | 41 ++++++++++++++------ src/Compilers/Named/WfFromUnit.v | 82 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 112 insertions(+), 11 deletions(-) create mode 100644 src/Compilers/Named/WfFromUnit.v (limited to 'src') diff --git a/src/Compilers/Named/Wf.v b/src/Compilers/Named/Wf.v index fec1de5ed..736d0bd81 100644 --- a/src/Compilers/Named/Wf.v +++ b/src/Compilers/Named/Wf.v @@ -1,3 +1,4 @@ +Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. @@ -11,27 +12,45 @@ Module Export Named. Context {var} (Context : @Context base_type_code Name var). - Fixpoint wff (ctx : Context) {t} (e : @exprf base_type_code op Name t) : option pointed_Prop - := match e with - | TT => Some trivial - | Var t n => match lookupb ctx n t return bool with - | Some _ => true - | None => false - end - | Op _ _ op args => @wff ctx _ args - | LetIn _ n ex _ eC => @wff ctx _ ex /\ inject (forall v, prop_of_option (@wff (extend ctx n v) _ eC)) - | Pair _ ex _ ey => @wff ctx _ ex /\ @wff ctx _ ey - end%option_pointed_prop. + Section gen. + Context (quantify : forall tx, (interp_flat_type var tx -> option pointed_Prop) -> option pointed_Prop). + Fixpoint wff_gen (ctx : Context) {t} (e : @exprf base_type_code op Name t) : option pointed_Prop + := match e with + | TT => Some trivial + | Var t n => match lookupb ctx n t return bool with + | Some _ => true + | None => false + end + | Op _ _ op args => @wff_gen ctx _ args + | LetIn _ n ex _ eC => @wff_gen ctx _ ex + /\ quantify _ (fun v => @wff_gen (extend ctx n v) _ eC) + | Pair _ ex _ ey => @wff_gen ctx _ ex /\ @wff_gen ctx _ ey + end%option_pointed_prop. + End gen. + + Definition wff := wff_gen (fun tx f => inject (forall v, prop_of_option (f v))). Definition wf (ctx : Context) {t} (e : @expr base_type_code op Name t) : Prop := forall v, prop_of_option (@wff (extend ctx (Abs_name e) v) _ (invert_Abs e)). End with_var. + Section unit. + Context (Context : @Context base_type_code Name (fun _ => unit)). + + Local Notation TT := (SmartValf _ (fun _ => tt) _). + Definition wff_unit := wff_gen Context (fun tx f => f TT). + Definition wf_unit ctx {t} (e : @expr base_type_code op Name t) : option pointed_Prop + := @wff_unit (extend ctx (Abs_name e) TT) _ (invert_Abs e). + End unit. + Definition Wf (Context : forall var, @Context base_type_code Name var) {t} (e : @expr base_type_code op Name t) := forall var, wf (Context var) empty e. End language. End Named. +Global Arguments wff_gen {_ _ _ _ _} quantify ctx {t} _. +Global Arguments wff_unit {_ _ _ _} ctx {t} _. +Global Arguments wf_unit {_ _ _ _} ctx {t} _. Global Arguments wff {_ _ _ _ _} ctx {t} _. Global Arguments wf {_ _ _ _ _} ctx {t} _. Global Arguments Wf {_ _ _} Context {t} _. diff --git a/src/Compilers/Named/WfFromUnit.v b/src/Compilers/Named/WfFromUnit.v new file mode 100644 index 000000000..c6b28f824 --- /dev/null +++ b/src/Compilers/Named/WfFromUnit.v @@ -0,0 +1,82 @@ +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Named.Context. +Require Import Crypto.Compilers.Named.ContextProperties. +Require Import Crypto.Compilers.Named.ContextDefinitions. +Require Import Crypto.Compilers.Named.Syntax. +Require Import Crypto.Compilers.Named.Wf. +Require Import Crypto.Util.PointedProp. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.SplitInContext. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.Option. + +Section language. + Context {base_type_code Name : Type} + {op : flat_type base_type_code -> flat_type base_type_code -> Type} + {base_type_code_dec : DecidableRel (@eq base_type_code)} + {Name_dec : DecidableRel (@eq Name)}. + + Section with_var. + Context {var} + (uContext : @Context base_type_code Name (fun _ => unit)) + (uContextOk : ContextOk uContext) + (vContext : @Context base_type_code Name var) + (vContextOk : ContextOk vContext). + + Local Ltac t := + repeat first [ progress simpl in * + | progress intros + | progress subst + | progress inversion_option + | congruence + | tauto + | solve [ eauto ] + | break_innermost_match_step + | break_innermost_match_hyps_step + | progress destruct_head'_and + | progress autorewrite with push_prop_of_option push_eq_Some_trivial in * + | rewrite !(@lookupb_extend base_type_code _ Name _) by auto + | rewrite (@find_Name_and_val_split base_type_code _ Name _) with (default := lookupb _ _) + | match goal with + | [ H : ?x = Some _ |- _ ] + => assert (x = None) by (split_iff; eauto); congruence + | [ |- _ /\ _ ] => split + | [ H : _ |- prop_of_option _ ] => eapply H; [ | eassumption ]; clear H + | [ |- context[find_Name_and_val ?tdec ?ndec ?b _ _ _ _ = None] ] + => rewrite <- !(@find_Name_and_val_None_iff _ tdec _ ndec _ b) + end ]. + + Lemma wff_from_unit + (vctx : vContext) + (uctx : uContext) + (Hctx : forall t n, lookupb vctx n t = None <-> lookupb uctx n t = None) + {t} (e : @exprf base_type_code op Name t) + : wff_unit uctx e = Some trivial -> prop_of_option (wff vctx e). + Proof using Name_dec base_type_code_dec uContextOk vContextOk. + revert uctx vctx Hctx; induction e; t. + Qed. + + Lemma wf_from_unit + (vctx : vContext) + (uctx : uContext) + (Hctx : forall t n, lookupb vctx n t = None <-> lookupb uctx n t = None) + {t} (e : @expr base_type_code op Name t) + : wf_unit uctx e = Some trivial -> wf vctx e. + Proof using Name_dec base_type_code_dec uContextOk vContextOk. + intros H ?; revert H; apply wff_from_unit; t. + Qed. + End with_var. + + Lemma Wf_from_unit + (Context : forall var, @Context base_type_code Name var) + (ContextOk : forall var, ContextOk (Context var)) + {t} (e : @expr base_type_code op Name t) + : wf_unit (Context:=Context _) empty e = Some trivial -> Wf Context e. + Proof using Name_dec base_type_code_dec. + intros H ?; revert H; apply wf_from_unit; auto; intros. + rewrite !lookupb_empty by auto; tauto. + Qed. +End language. + +Hint Resolve wf_from_unit Wf_from_unit wff_from_unit : wf. -- cgit v1.2.3