The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi,

Well to my knowledge, "consistency" is not defined in Coq.

If what you mean is how to prove inconsistency from 0=1

without going through False, this is a way, by pattern

matching which is essentially a decomposition of

what "discriminate" does.

Section absurdum.

  Fact zero_eq_one_absurd : 0 = 1 -> forall P : Prop, P.
  Proof.
    intros H P.
    set (f := fun n => match n with 0 => True | _ => P end).
    change (f 1).
    rewrite <- H.
    exact I.
  Qed.

End absurdum.

Check zero_eq_one_absurd.

It also works as is for (P : Type) at the cost of "singleton

elimination" (SE). But it can also be done for P:Type

w/o SE. It is a bit more complicated though.

Best,

Dominique

---

De: "Patricia Peratto" <psperatto AT vera.com.uy>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Dimanche 2 Février 2020 01:16:55
Objet: [Coq-Club] consistency

Can not be defined that different constructors are 

different terms automatically?

To not use bottom to prove 0<>1.

To be consistent.

Regards,

Patricia Peratto