diff options
author | Jason Gross <jgross@mit.edu> | 2018-11-15 17:47:47 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-11-15 17:47:47 -0500 |
commit | 043c530ffec38d5c54271d58c484452bd9dd469d (patch) | |
tree | 4f2432dcbfb9e2ef9839030605dc34e0f0cb52b1 | |
parent | 5549dcda8833de957efa14cd59fe22f2a33de683 (diff) |
Add UnderLets.wf_interp_Proper
-rw-r--r-- | src/Experiments/NewPipeline/UnderLetsProofs.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/UnderLetsProofs.v b/src/Experiments/NewPipeline/UnderLetsProofs.v index 837aba4b4..101d7e9dd 100644 --- a/src/Experiments/NewPipeline/UnderLetsProofs.v +++ b/src/Experiments/NewPipeline/UnderLetsProofs.v @@ -353,6 +353,25 @@ Module Compilers. : expr.interp ident_interp (interp (of_expr x)) = expr.interp ident_interp x. Proof. induction x; cbn [expr.interp interp of_expr]; cbv [LetIn.Let_In]; eauto. Qed. End for_interp. + + Section for_interp2. + Context {base_interp1 base_interp2 : base_type -> Type} + {ident_interp1 : forall t, ident t -> type.interp base_interp1 t} + {ident_interp2 : forall t, ident t -> type.interp base_interp2 t}. + + Lemma wf_interp_Proper {T1 T2} + {P : list { t : type & type.interp base_interp1 t * type.interp base_interp2 t }%type -> T1 -> T2 -> Prop} + {G v1 v2} + (Hwf : @wf _ _ T1 T2 P G v1 v2) + : exists seg, P (seg ++ G) (interp ident_interp1 v1) (interp ident_interp2 v2). + Proof using Type. + induction Hwf; [ exists nil; cbn [List.app]; assumption | ]. + let H := match goal with H : forall v1 v2, ex _ |- _ => H end in + edestruct H as [seg ?]; eexists (seg ++ [_]). + rewrite <- List.app_assoc; cbn [List.app]. + eassumption. + Qed. + End for_interp2. End with_ident. Section reify. |