The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Hi Fred,

in this case you are lucky: the proposition <= is proof irrelevant, i.e. 
any two proofs p,q : x <= y are provably equal. To that end, you can 
prove (without having to assume proof irrelevance):

  coord, c1 = c2 <-> proj1_sig c1 = proj1_sig c2.

See below for a proof.

An alternative is to encode your type as:

  { x | Is_true (b x) }

where b : nat -> bool is a boolean predicate. It is trivial to show that 
Is_true is proof irrelevant, and thus to prove a property as above.

Robbert

===============

Require Import Eqdep Eqdep_dec Omega.

Lemma nat_le_pi: forall (x y : nat) (p q : x <= y), p = q.
Proof.
  assert (forall x y (p : x <= y) y' (q : x <= y'),
    y = y' -> eq_dep nat (le x) y p y' q) as aux.
  { fix 3. intros x ? [|y p] ? [|y' q].
  - easy.
  - clear nat_le_pi. omega.
  - clear nat_le_pi. omega.
  - injection 1. intros Hy. now case (nat_le_pi x y p y' q Hy). }
    intros x y p q. now apply (eq_dep_eq_dec eq_nat_dec), aux.
Qed.

Definition coord := { x | x>0 /\ x <= 3}.

Lemma coord_eq : forall c1 c2 : coord, c1 = c2 <-> proj1_sig c1 = 
proj1_sig c2.
Proof.
  intros c1 c2; split; [now intros ->|].
  destruct c1 as [x [Hx Hx']], c2 as [y [Hy Hy']]; simpl; intros ->.
  f_equal; f_equal; apply nat_le_pi.
Qed.

Print Assumptions coord_eq.
(* Closed under the global context *)

On 05/28/2016 01:24 AM, Fred Smith wrote:
> Hi all,
>
> I wanted to define a small range of numbers and thought this would be a
> clean solution:
>
>     Definition coord := { x | x>0 /\ x <= 3}.
>
> Then I can define the 3 valid coordinates:
>
>    Definition c1 : coord := coord1.
>      refine (exist _ 1 _).
>      lia.
>    Defined.
>    Definition c2 : coord.
>      refine (exist _ 2 _).
>      lia.
>    Defined.
>    Definition c3 : coord.
>      refine (exist _ 3 _).
>      lia.
>    Defined.
>
> Now I would like to prove:
>
>    Lemma coord_all_wish:
>      forall c:coord, c=c1 \/ c=c2 \/ c=c3.
> Of course this statement is not true, because there are an infinite
> number of proofs that c1 satisfies the specification.  What I really
> mean is proj1_sig c = proj1_sig c1, ...
>
> I was originally viewing this coord type as morally equivalent to the
> inductive type c1 | c2 | c3 but with the added benefit that I could make
> 3 a parameter n and the design would scale.  Now, I see that using this
> design makes "forall" arguments about coordinates quite painful because
> it precludes direct case analysis.
>
> In summary I would like a type parametrized by n that when n is known
> has n distinguishable inhabitants.
>
> Is Fin.t the answer to this question?  Or does everything magically
> evaporate if I am willing to invoke proof irrelevance?  Or is there some
> magic encoding I haven't thought of?
>
> Thanks for any help.
>
> -Fred