diff options
Diffstat (limited to 'MenhirLib/Validator_classes.v')
-rw-r--r-- | MenhirLib/Validator_classes.v | 74 |
1 files changed, 74 insertions, 0 deletions
diff --git a/MenhirLib/Validator_classes.v b/MenhirLib/Validator_classes.v new file mode 100644 index 00000000..c043cb73 --- /dev/null +++ b/MenhirLib/Validator_classes.v @@ -0,0 +1,74 @@ +(****************************************************************************) +(* *) +(* Menhir *) +(* *) +(* Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud *) +(* *) +(* Copyright Inria. All rights reserved. This file is distributed under *) +(* the terms of the GNU Lesser General Public License as published by the *) +(* Free Software Foundation, either version 3 of the License, or (at your *) +(* option) any later version, as described in the file LICENSE. *) +(* *) +(****************************************************************************) + +From Coq Require Import List. +From Coq.ssr Require Import ssreflect. +Require Import Alphabet. + +Class IsValidator (P : Prop) (b : bool) := + is_validator : b = true -> P. +Hint Mode IsValidator + -. + +Instance is_validator_true : IsValidator True true. +Proof. done. Qed. + +Instance is_validator_false : IsValidator False false. +Proof. done. Qed. + +Instance is_validator_eq_true b : + IsValidator (b = true) b. +Proof. done. Qed. + +Instance is_validator_and P1 b1 P2 b2 `{IsValidator P1 b1} `{IsValidator P2 b2}: + IsValidator (P1 /\ P2) (if b1 then b2 else false). +Proof. split; destruct b1, b2; auto using is_validator. Qed. + +Instance is_validator_comparable_leibniz_eq A (C:Comparable A) (x y : A) : + ComparableLeibnizEq C -> + IsValidator (x = y) (compare_eqb x y). +Proof. intros ??. by apply compare_eqb_iff. Qed. + +Instance is_validator_comparable_eq_impl A `(Comparable A) (x y : A) P b : + IsValidator P b -> + IsValidator (x = y -> P) (if compare_eqb x y then b else true). +Proof. + intros Hval Val ->. rewrite /compare_eqb compare_refl in Val. auto. +Qed. + +Lemma is_validator_forall_finite A P b `(Finite A) : + (forall (x : A), IsValidator (P x) (b x)) -> + IsValidator (forall (x : A), P x) (forallb b all_list). +Proof. + move=> ? /forallb_forall. + auto using all_list_forall, is_validator, forallb_forall. +Qed. +(* We do not use an instance directly here, because we need somehow to + force Coq to instantiate b with a lambda. *) +Hint Extern 2 (IsValidator (forall x : ?A, _) _) => + eapply (is_validator_forall_finite _ _ (fun (x:A) => _)) + : typeclass_instances. + +(* Hint for synthetizing pattern-matching. *) +Hint Extern 2 (IsValidator (match ?u with _ => _ end) ?b0) => + let b := fresh "b" in + unshelve notypeclasses refine (let b : bool := _ in _); + [destruct u; intros; shelve|]; (* Synthetize `match .. with` in the validator. *) + unify b b0; + unfold b; destruct u; clear b + : typeclass_instances. + +(* Hint for unfolding definitions. This is necessary because many + hints for IsValidator use [Hint Extern], which do not automatically + unfold identifiers. *) +Hint Extern 100 (IsValidator ?X _) => unfold X + : typeclass_instances. |