From 7a9faafa8a3507bc20ae15bbe71200d9c4b5a12b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 30 Oct 2016 12:35:06 -0400 Subject: Generalize InputSyntax.Compile_correct --- src/Reflection/InputSyntax.v | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) (limited to 'src/Reflection/InputSyntax.v') diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v index 15f7515b3..1c97d2174 100644 --- a/src/Reflection/InputSyntax.v +++ b/src/Reflection/InputSyntax.v @@ -105,18 +105,23 @@ Section language. end. Qed. - Lemma Compile_correct {t : flat_type} (e : @Expr t) - : Syntax.Interp interp_op (Compile e) = Interp interp_op e. + Lemma Compile_correct {t} (e : @Expr t) + : interp_type_gen_rel_pointwise (fun _ => @eq _) + (Syntax.Interp interp_op (Compile e)) + (Interp interp_op e). Proof. unfold Interp, Compile, Syntax.Interp; simpl. pose (e interp_flat_type) as E. repeat match goal with |- context[e ?f] => change (e f) with E end. - refine match E with - | Abs _ _ _ => fun x : Prop => x (* small inversions *) - | Return _ _ => _ - end. - apply compilef_correct. + clearbody E; clear e. + induction E. + { apply compilef_correct. } + { simpl; auto. } Qed. + + Lemma Compile_flat_correct {t : flat_type} (e : @Expr t) + : Syntax.Interp interp_op (Compile e) = Interp interp_op e. + Proof. exact (@Compile_correct t e). Qed. End compile_correct. End expr_param. End language. -- cgit v1.2.3