diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-28 18:54:55 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-28 18:55:53 -0400 |
| commit | 20d1a5816a33568f2fe13e28445396c476a49d27 (patch) | |
| tree | e34a378bd9a499387a74660c40cccea3ee176df6 /src/Reflection/MapCastByDeBruijnWf.v | |
| parent | 1777daf558ae09e73f88ff85cc7a44f804c49193 (diff) | |
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
Diffstat (limited to 'src/Reflection/MapCastByDeBruijnWf.v')
| -rw-r--r-- | src/Reflection/MapCastByDeBruijnWf.v | 7 |
1 files changed, 3 insertions, 4 deletions
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. |