The Coq mailing list

["Rui Baptista" <rui.baptista AT mail.com>]

(* You can also work instead with the predicate behind the function. *)

 

Conjecture Z : Set.
Conjecture sub : Z -> Z -> Z.
Conjecture leq : Z -> Z -> Prop.

 

Infix "-" := sub : Z_scope.
Infix "<=" := leq : Z_scope.

 

Delimit Scope Z_scope with Z.

 

Require Import Coq.Setoids.Setoid.

 

Conjecture C1 : forall P, True /\ P <-> P.
Conjecture C2 : forall P, P /\ True <-> P.
Conjecture C3 : forall A (x : A), x = x <-> True.
Conjecture C4 : forall i j, (i <= j)%Z \/ (j <= i)%Z <-> True.

 

Hint Rewrite C1 C2 C3 C4 : Hints.

 

Definition diff : Z -> Z -> Z -> Prop := fun i j k => (i <= j)%Z /\ (i - j)%Z = k.

 

Goal forall i j, diff i j (i - j)%Z \/ diff j i (j - i)%Z.
unfold diff; repeat (firstorder; autorewrite with Hints in *).

Qed.

 

(* If you want to compose your partial functions, you can refactor them to not just return predicates but also take them as input. If they are undefined for a certain input, they return the empty predicate, if they are defined, they return a singleton predicate, and if you want to, you can also return multiple values. *)

Definition singleton : forall {A}, A -> (A -> Prop) := @eq.

Definition equal : forall {A}, (A -> Prop) -> (A -> Prop) -> Prop := fun A P Q => forall x, P x <-> Q x.

Notation "{{ x }}" := (singleton x) (at level 0).

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

 

Definition diff2 : (Z -> Prop) -> (Z -> Prop) -> (Z -> Prop) := fun P Q i => exists j k, P j /\ Q k /\ diff j k i.

 

Goal forall i j, diff2 {{i}} {{j}} == {{(i - j)%Z}} \/ diff2 {{j}} {{i}} == {{(j - i)%Z}}.
Admitted.

 

(* Regards, Rui *)