1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
(****************************************************************************)
(* *)
(* 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.
Global Hint Mode IsValidator + - : typeclass_instances.
Global Instance is_validator_true : IsValidator True true.
Proof. done. Qed.
Global Instance is_validator_false : IsValidator False false.
Proof. done. Qed.
Global Instance is_validator_eq_true b :
IsValidator (b = true) b.
Proof. done. Qed.
Global Instance is_validator_and P1 b1 P2 b2 `{IsValidator P1 b1} `{IsValidator P2 b2}:
IsValidator (P1 /\ P2) (if b1 then b2 else false).
Proof. by split; destruct b1, b2; apply is_validator. Qed.
Global 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.
Global 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 Hb ?.
apply is_validator, Hb, all_list_forall.
Qed.
(* We do not use an instance directly here, because we need somehow to
force Coq to instantiate b with a lambda. *)
Global Hint Extern 2 (IsValidator (forall x : ?A, _) _) =>
eapply (is_validator_forall_finite _ _ (fun (x:A) => _))
: typeclass_instances.
(* Hint for synthetizing pattern-matching. *)
Global 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. *)
Global Hint Extern 100 (IsValidator ?X _) => unfold X
: typeclass_instances.
|
