The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

Like Spiwack wrote, if you have a relation, you can turn it into a function from sets to a set. If the relation represents a total function and the inputs are singleton sets then it will behave like expected. If the function is partial you might have to add some preconditions to your theorems. I don't know what happens if the relation isn't a function. See also the last chapter of the manual for how to conveniently rewrite with equivalence relations.

Set Implicit Arguments.

Unset Strict Implicit.

Set Contextual Implicit.

Set Reversible Pattern Implicit.

Set Maximal Implicit Insertion.

Definition set : Type -> Type := fun t1 => t1 -> Prop.

Definition singleton : forall t1 : Type, t1 -> set t1 := fun t1 x1 x2 => forall p1 : t1 -> Prop, p1 x1 -> p1 x2.

Notation "`" := singleton.

Definition subset : forall t1, set t1 -> set t1 -> Prop := fun _ p1 p2 => forall x1, p1 x1 -> p2 x1.

Definition equal : forall t1, set t1 -> set t1 -> Prop := fun _ s1 s2 => subset s1 s2 /\ subset s2 s1.

Infix "==" := equal (at level 70).

Definition functionalize : forall t1, (t1 -> t1 -> t1 -> Prop) -> set t1 -> set t1 -> set t1 := fun _ r1 p1 p2 x1 => forall x2 x3, p1 x2 -> p2 x3 -> r1 x2 x3 x1.

Inductive preaddition (n1 : nat) : nat -> nat -> Prop :=

  | preaddition_zero : preaddition n1 0 n1

  | preaddition_successor : forall n2 n3, preaddition n1 n2 n3 -> preaddition n1 (S n2) (S n3).

Hint Constructors preaddition.

Axiom a1 : forall n1 n2, preaddition n1 0 n2 -> n1 = n2.

Hint Resolve a1.

Definition addition : set nat -> set nat -> set nat := functionalize preaddition.

Infix "+" := addition.

Lemma addition_zero : forall n1, ` n1 + ` 0 == ` n1.

Proof.

unfold equal, addition, singleton, subset, functionalize. split.

intros. assert (n1 = x1) by info_eauto. rewrite <- H1. eauto.

intros. change ((fun x2 => preaddition x2 x3 x1) x2). eapply H0. change ((fun x3 => preaddition n1 x3 x1) x3). eapply H1. change ((fun x1 => preaddition n1 0 x1) x1). eapply H. eauto.

Qed.

Regards.

On Mon, Jan 27, 2014 at 3:22 PM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

On 27/01/2014 16:13, Arnaud Spiwack wrote:

 >> Definition extension2 f x y := exists a, exists b, x a -> x b -> f a b
 >
 >
 > Unfortunately no.
 > In Why3, we display a warning whenever the user writes this kind of
predicate ; it has been helpful to debug some broken specifications
early. It might be worth having the same warning message in Coq.

I'm confused. Apart from the fact that I forgot an obvious lambda (f is
supposed to be of type A->B->(X->Prop)), this definition is a correct
binary extension for the powerset monad. Could you elaborate on the
issue you have with it?

My issue is that this kind of predicate is (almost) always a tautology, which makes it pointless. So I doubt it is what you intended to write in the first place. Didn't you mean the following instead?

Definition extension2 f x y := exists a, exists b, x a /\ x b /\ f a b.

Best regards,

Guillaume