The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

(* Copy Paste in CoqIDE/ProofGeneral to follow along *)
(*
I came across the same problem a couple weeks ago, when trying to
relate a function and a relation that contains this function, ie for
a function [f : t1 -> ... -> tn -> t], and a relation
[f_spec : t1 -> ... tn -> t -> Prop] which shall be seen as a relation
between the inputs and the output, I want a compatibility lemma
[f_dec : forall x1 .. xn, f_spec x1 .. xn (f x1 .. xn)]. This is a general
way of specifying a function and in particular is more general than what
you're trying to do. Here is what I ended up doing :
*)
Require Import List.
Fixpoint arrows (l : list Type) (res : Type) : Type :=
  match l with
  | nil => res
  | t::q => t -> (arrows q res)
  end.

Fixpoint compatible (l : list Type) (res : Type) :
  arrows l res -> arrows l (res -> Prop) -> Prop :=
  match l as a return arrows a res -> arrows a (res -> Prop) -> Prop with
  | nil => fun f f_spec => f_spec f
  | t::q => fun f f_spec => forall x : t, compatible q res (f x) (f_spec x)
  end.

(* And a class to put the spec and the lemma together *)
Class View (l : list Type) (res : Type) (f : arrows l res) := {
  f_spec : arrows l (res -> Prop);
  f_dec : compatible l res f f_spec
}.

(* There is one drawback in this method for dealing with arity, its the
   fact that for a given [f] of type [t1 -> t2 -> ... -> tn], Coq will
   be unable to infer [l] and [res] such that [f : arrows l res]. But
   you can do it with Ltac (the same way you used Ltac to find the
   arity of [f]), I also had to use Ltac at that point in order to
   help Coq automatically find instances of [View] and design a general
   tactic to use these specifications whenever they are available for a
   given function symbol [f].
*)

(* In your particular case, you probably don't want that whole machinery
   but you could try something like this, it would be easier to use
   than your [implements] predicates. First you define an inductive
   to relate [bool] and [Prop] :
*)
Inductive decides (P : Prop) : bool -> Prop :=
| decides_true : forall (Htrue : P), decides P true
| decides_false : forall (Hfalse : ~P), decides P false.

Lemma decides_1 : forall P b, decides P b -> b = true -> P.
Proof.
  intros P b H; destruct H; auto; intro; discriminate.
Qed.
Lemma decides_2 : forall P b, decides P b -> b = false -> ~P.
Proof.
  intros P b H; destruct H; auto; intro; discriminate.
Qed.
Implicit Arguments decides_1 [P b].
Implicit Arguments decides_2 [P b].

(* And then a generic [implements] in a similar fashion to
   the [compatible] predicate above : *)
Fixpoint implements (l : list Type) :
  arrows l Prop -> arrows l bool -> Prop :=
  match l as a return arrows a Prop -> arrows a bool -> Prop with
    | nil => fun P f => decides P f
    | t::q => fun P f => forall x : t, implements q (P x) (f x)
  end.

(* Lets try it out on the [le] predicate on naturals : *)
Require Import Arith.
Definition tcons := (@cons Type).
Definition tnil := (@nil Type).
Section example.
  Definition is_le (n m : nat) := if le_lt_dec n m then true else false.
  Lemma implements_le : implements (tcons nat (tcons nat tnil)) le is_le.
  Proof.
    simpl; intros x y; unfold is_le.
    destruct (le_lt_dec x y); constructor; auto with arith.
  Qed.

  (* There are basically 2 kinds of situations when you want to use the
     fact that a predicate is decided by a certain function.
     - if you know [P] (resp. [~P]), you know that [f = true] (resp.
[f = false])
     - you want to have [P] (resp. [~P]) in a context where you can prove
     or compute that [f = true] (resp. [f = false])
     In the first case, just destruct the [implements] predicate ; and in the
     second case you can use the [decides_1] and [decides_2]
predicates. Following
     are examples of this :
     *)
  Goal forall x y, le x y -> is_le x y = true.
  Proof.
    intros; destruct (implements_le x y); auto.
  Qed.
  Goal forall x y, is_le x y = true -> le x y.
  Proof.
    intros; apply (decides_1 (implements_le _ _)); auto.
  Qed.
  Goal ~le 4 3.
  Proof.
    apply (decides_2 (implements_le _ _)); reflexivity.
  Qed.

  (* Of course, it is still not completely satisfactory, since you'd
     want [implements_le] in the [decides_1] and [decides_2] lemmas
     to be inferred from the head of the goal. In the first case as well,
     we'd rather have a call like [decides le] or [decides le x y] instead
     of having to specify [implements_le] explicitely.

     One solution is to use typeclasses, and a class similar to my [View]
     class above, but again you will have to use some Ltac magic in order
     to guess the arity and [list Type] necessary for a given function symbol
     and the whole thing is a bit tedious. This is doable but too long to be
     included here.
     Another possibility, if you don't have that many different predicates
     but each of them is used very often, is to use Tactic Notations :
     *)
  Tactic Notation "decides" "is_le" constr(x) constr(y) :=
    destruct (implements_le x y).
  Tactic Notation "decides" "is_le" := (* infer x and y from the context *)
    match goal with
      | |- context f [is_le ?X ?Y] => destruct (implements_le X Y)
      | H : context f [is_le ?X ?Y] |- _ => destruct (implements_le X Y)
      | _ => fail 2 "No instance of le found in the context"
    end.
  Tactic Notation "decides" "le" :=
    match goal with
      | |- le ?X ?Y => apply (decides_1 (implements_le X Y)); try reflexivity
      | |- ~le ?X ?Y => apply (decides_2 (implements_le X Y)); try reflexivity
      | _ => fail 2 "Goal should be of the form 'le _ _' or '~le _ _'"
    end.
  (* These are only some of the possibilities, just pick or make the one that
     suits your needs. You would have to define new similar tactics for each
     of the predicates you are interested in, though. *)

  Goal forall x y, le x y -> is_le x y = true.
  Proof.
    intros; decides is_le; auto.
  Qed.
  Goal forall x y, is_le x y = true -> le x y.
  Proof.
    intros; decides le; auto.
  Qed.
  Goal ~le 4 3.
  Proof.
    decides le.
  Qed.
End example.

(* This ended up being much longer than I expected, but I hope this helps. *)

--
Stéphane L.

On Wed, Apr 14, 2010 at 9:23 AM, Eric Jaeger 
<eric.jaeger AT ssi.gouv.fr>
 wrote:
> Hi all,
>
> I'm currently trying to revisit some Coq code to improve automation
> (digging further in Ltac) and notations. I've for example several
> definitions to relate a predicate and a boolean function deciding this
> predicate:
>
> Definition implements1(T:Type)(P:T->Type)(f:T->bool):=
>  ((forall (t:T), f t=true->P t) * (forall (t:T), f t=false->P
> t->False))%type.
>
> Definition implements2(T1 T2:Type)(P:T1->T2->Type)(f:T1->T2->bool):=
>  ((forall (t1:T1)(t2:T2), f t1 t2=true->P t1 t2) *
>  (forall (t1:T1)(t2:T2), f t1 t2=false->P t1 t2->False))%type.
>
> ...
>
> That is, one definition per arity.
>
> 1/ Is there an elegant way to merge these definitions (possibly
> internally relying  on currification, but noting that I do not want to
> use A*B->C instead of A->B->C at top level) ?
>
> 2/ If not, is there a way to use some forms of "polymorphic" coercions
> (e.g. a generic currification) ?
>
> 3/ If not, is there a way to define a single notation for all these
> definitions? E.g. "P>>>f" would mean "implem1 P f" or "implem2 P f",
> etc., according to the arity of P.
>
> 4/ If not, is there a way to use Ltac to define interesting tactics to
> address my problem? I've already a tactic "arity" returning the number
> of variables for a predicate/boolean function, but I've not discovered
> any way to use it to solve my problem.
>
>  Thanks in advance for any answer, Eric
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06