The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 19 oct. 09 à 09:44, Thomas Braibant a écrit :

<snip/>

> The goal here would be to be able to automatize such destructions, in
> order to be able to reason more easily on more complicated programs. I
> wonder if any function should have such a specification (like add,
> below).
> Inductive add_spec : elt -> t -> t -> Type :=
> | add_spec_1 : forall x s s', (forall y, In y s' <-> (E.eq x y \/ In y
> s)) -> add_spec x s s'.
> Lemma add_eq : forall x s, add_spec x s (add x s).

Hi Thomas,

You're basically building propositional views of your functions and want
to automate the transformation from bool to Prop. You can do that with
minimal verbosity using type classes, a few Ltac tricks and dependent
elimination (or, I suppose, using ssreflect's support for reflection
and dependent elimination). Here's my attempt:

<<

Require Import Equality Program FSets.
Require Import Sumbool.
Module Test (X : FSetInterface.S).
 Module OrdProps := FSetProperties.OrdProperties X.
 Module EqProps := FSetEqProperties.EqProperties X.
 Module Props := EqProps.MP.
 Module Facts  := Props.FM.
 Module Dec := Props.Dec.

 Include Facts.
 Include OrdProps.
 Import  X.
 Ltac setdec := Dec.fsetdec.

 Definition proj_sumbool {P Q} (x : {P} + {Q}) :=
   if x then true else false.

 Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1
else 2)= 1.
   intros.
   case_eq (mem z (add x (add y (singleton z)))); intro H.
     reflexivity.
     apply False_ind. revert H. rewrite <- not_mem_iff. set_iff.  
intuition.
 Qed.
 Lemma mem_dec : forall x s, {In x s} + {~ In x s}. Admitted.
 Lemma mem_proj : forall x s, mem x s = proj_sumbool (mem_dec x s).   
Admitted.

 Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1
else 2)= 1.
   intros.
   rewrite mem_proj. destruct mem_dec. reflexivity.
   apply False_ind. apply n. set_iff. intuition.
 Qed.

 Inductive mem_spec_ind : elt -> t -> bool -> Prop :=
   | mem_spec_1 : forall x s, In x s -> mem_spec_ind x s true
   | mem_spec_2 : forall x s, ~In x s -> mem_spec_ind x s false.
 Lemma mem_eq : forall x s, mem_spec_ind x s (mem x s). Admitted.


 (* Apply dependent elimination to a term *)
 Ltac depelim_term t := let H := fresh in
   set (H := t) ; depelim H ;
     (* Rewrite with the last hyp that gives the equality between
        the result and the initial call *)
     try on_last_hyp ltac:(fun id => rewrite <- id ; clear id).

 Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1
   else 2)= 1.
   intros. depelim_term (mem_eq z (add x (add y (singleton z)))).
   reflexivity. apply False_ind. apply H. setdec.
 Qed.

 (* Go further and add a class for propositional views of
    functions. This is kind of a dummy class as we can't
    express the form a view type should have here,
    but [prop_view_ty] should be [Π Δ, some_ind Δ (f Δ)]. *)

 Class PropView {A} (f : A) :=
   { prop_view_ty : Prop ; prop_view : prop_view_ty }.

 Instance mem_propview : PropView mem := { prop_view := mem_eq }.

 (* Now a tactic to destruct a call to a function using
    his associated propositional view. *)

 Ltac prop_view f :=
   (* Find the view associated with [f] *)
   let prf := constr:(prop_view (f:=f)) in
     on_call f ltac:(fun c =>
       match c with
         | appcontext args [ f ] =>
           let ind_app := context args [ prf ] in
           let H := fresh in
           let call := fresh in
             set(H := ind_app) ; (* The view proof *)
             set(call := c) in *; (* Abstract the call *)
             depelim H
       end).

 Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1
else 2)= 1.
   intros. prop_view mem.
   reflexivity. apply False_ind. apply H. setdec.
 Qed.

 Inductive add_spec : elt -> t -> t -> Type :=
 | add_spec_1 : forall x s s', (forall y, In y s' <-> (E.eq x y \/ In
y s)) -> add_spec x s s'.

 Lemma add_eq : forall x s, add_spec x s (add x s).
 Proof.
   intros.
   constructor.  intros. set_iff. reflexivity.
 Qed.

End Test.

>>

Hope this helps,
-- Matthieu