From 647cc8dc9699277cb1e77ae3b07c007186720d59 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 26 Dec 2016 16:55:06 +0100 Subject: Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.v Applied to the 92-constructor 'operation' type, 'decide equality' produces a huge transparent term that causes the VM compiler to generate huge code and exceeed a memory limit of Coq on 32-bit platforms. (The limit is OCaml's, really.) The lib/BoolEqual.v file defines alternative tactics to build decidable equalities where the transparent part of the definition is smaller (O(N^2) instead of O(N^3)). The proof parts are still huge (O(N^3)) but they are opaque. Fixes #151 --- lib/BoolEqual.v | 167 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 167 insertions(+) create mode 100644 lib/BoolEqual.v (limited to 'lib/BoolEqual.v') diff --git a/lib/BoolEqual.v b/lib/BoolEqual.v new file mode 100644 index 00000000..a5b543e1 --- /dev/null +++ b/lib/BoolEqual.v @@ -0,0 +1,167 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Tactics to generate Boolean-valued equalities *) + +(** The [decide equality] tactic can generate a term of type +[forall (x y: A), {x=y} + {x<>y}] if [A] is an inductive type. +This term is a decidable equality function. + +Similarly, this module defines a [boolean_equality] tactic that generates +a term of type [A -> A -> bool]. This term is a Boolean-valued equality +function over the inductive type [A]. Two internal tactics generate +proofs that show the correctness of this equality function [f], namely +proofs of the following two properties: +- [forall (x: A), f x x = true] +- [forall (x y: A), f x y = true -> x = y] + +Finally, the [decide_equality_from f] tactic wraps [f] (the Boolean equality +generated by [boolean_equality]) and those proofs together, producing +a decidable equality of type [forall (x y: A), {x=y} + {x<>y}]. + +The advantage of the present tactics over the standard [decide equality] +tactic is that the former produce smaller transparent definitions than +the latter. + +For a type [A] that has N constructors, [decide equality] produces a +single term of size O(N^3), which must be kept transparent so that +it computes and extracts as expected. Given such a big transparent +definition, the virtual machine compiler of Coq produces very big +chunks of VM code, causing memory overflows on 32-bit platforms. + +In contrast, the term produced by [boolean_equality] has size O(N^2) +only (so to speak). The proofs that this term is a correct boolean +equality are still O(N^3), but those proofs are opaque and do not need +to be compiled to VM code. Only the boolean equality itself is defined +transparently and compiled. + +The present tactics also have some restrictions: +- Constructors must have at most 4 arguments. +- Decidable equalities must be provided (as hypotheses in the context) + for all the types [T] of constructor arguments other than type [A]. +- They probably do not work for mutually-defined inductive types. +*) + +Require Import Coqlib. + +Module BE. + +Definition bool_eq {A: Type} (x y: A) : Type := bool. + +Ltac bool_eq_base x y := + change (bool_eq x y); + match goal with + | [ H: forall (x y: ?A), bool |- @bool_eq ?A x y ] => exact (H x y) + | [ H: forall (x y: ?A), {x=y} + {x<>y} |- @bool_eq ?A x y ] => exact (proj_sumbool (H x y)) + | _ => idtac + end. + +Ltac bool_eq_case := + match goal with + | |- bool_eq (?C ?x1 ?x2 ?x3 ?x4) (?C ?y1 ?y2 ?y3 ?y4) => + refine (_ && _ && _ && _); [bool_eq_base x1 y1|bool_eq_base x2 y2|bool_eq_base x3 y3|bool_eq_base x4 y4] + | |- bool_eq (?C ?x1 ?x2 ?x3) (?C ?y1 ?y2 ?y3) => + refine (_ && _ && _); [bool_eq_base x1 y1|bool_eq_base x2 y2|bool_eq_base x3 y3] + | |- bool_eq (?C ?x1 ?x2) (?C ?y1 ?y2) => + refine (_ && _); [bool_eq_base x1 y1|bool_eq_base x2 y2] + | |- bool_eq (?C ?x1) (?C ?y1) => bool_eq_base x1 y1 + | |- bool_eq ?C ?C => exact true + | |- bool_eq _ _ => exact false + end. + +Ltac bool_eq := + match goal with + | [ |- ?A -> ?A -> bool ] => + let f := fresh "rec" in let x := fresh "x" in let y := fresh "y" in + fix f 1; intros x y; change (bool_eq x y); destruct x, y; bool_eq_case + | [ |- _ -> _ ] => + let eq := fresh "eq" in intro eq; bool_eq + end. + +Lemma proj_sumbool_is_true: + forall (A: Type) (f: forall (x y: A), {x=y} + {x<>y}) (x: A), + proj_sumbool (f x x) = true. +Proof. + intros. unfold proj_sumbool. destruct (f x x). auto. elim n; auto. +Qed. + +Ltac bool_eq_refl_case := + match goal with + | [ |- true = true ] => reflexivity + | [ |- proj_sumbool _ = true ] => apply proj_sumbool_is_true + | [ |- _ && _ = true ] => apply andb_true_iff; split; bool_eq_refl_case + | _ => auto + end. + +Ltac bool_eq_refl := + let H := fresh "Hrec" in let x := fresh "x" in + fix H 1; intros x; destruct x; simpl; bool_eq_refl_case. + +Lemma false_not_true: + forall (P: Prop), false = true -> P. +Proof. + intros. discriminate. +Qed. + +Lemma proj_sumbool_true: + forall (A: Type) (x y: A) (a: {x=y} + {x<>y}), + proj_sumbool a = true -> x = y. +Proof. + intros. destruct a. auto. discriminate. +Qed. + +Ltac bool_eq_sound_case := + match goal with + | [ H: false = true |- _ ] => exact (false_not_true _ H) + | [ H: _ && _ = true |- _ ] => apply andb_prop in H; destruct H; bool_eq_sound_case + | [ H: proj_sumbool ?a = true |- _ ] => apply proj_sumbool_true in H; bool_eq_sound_case + | [ |- ?C ?x1 ?x2 ?x3 ?x4 = ?C ?y1 ?y2 ?y3 ?y4 ] => apply f_equal4; auto + | [ |- ?C ?x1 ?x2 ?x3 = ?C ?y1 ?y2 ?y3 ] => apply f_equal3; auto + | [ |- ?C ?x1 ?x2 = ?C ?y1 ?y2 ] => apply f_equal2; auto + | [ |- ?C ?x1 = ?C ?y1 ] => apply f_equal; auto + | [ |- ?x = ?x ] => reflexivity + | _ => idtac + end. + +Ltac bool_eq_sound := + let Hrec := fresh "Hrec" in let x := fresh "x" in let y := fresh "y" in + fix Hrec 1; intros x y; destruct x, y; simpl; intro; bool_eq_sound_case. + +Lemma dec_eq_from_bool_eq: + forall (A: Type) (f: A -> A -> bool) + (f_refl: forall x, f x x = true) (f_sound: forall x y, f x y = true -> x = y), + forall (x y: A), {x=y} + {x<>y}. +Proof. + intros. destruct (f x y) eqn:E. + left. apply f_sound. auto. + right; red; intros. subst y. rewrite f_refl in E. discriminate. +Defined. + +End BE. + +(** Applied to a goal of the form [t -> t -> bool], the [boolean_equality] + tactic defines a function with that type, returning [true] iff the two + arguments of type [t] are equal. [t] must be an inductive type. + For any type [u] other than [t] that appears in arguments of constructors + of [t], a decidable equality over [u] must be provided, as an hypothesis + of type [forall (x y: u), {x=y}+{x<>y}]. *) +Ltac boolean_equality := BE.bool_eq. + +(** Given a function [beq] of type [t -> t -> bool] produced by [boolean_equality], + the [decidable_equality_from beq] produces a decidable equality with type + [forall (x y: t], {x=y}+{x<>y}. *) + +Ltac decidable_equality_from beq := + apply (BE.dec_eq_from_bool_eq _ beq); [abstract BE.bool_eq_refl|abstract BE.bool_eq_sound]. -- cgit