coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Both annoying things in one place
Date: Mon, 13 Mar 2017 11:18:43 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ilmars.cirulis AT gmail.com; spf=Pass smtp.mailfrom=ilmars.cirulis AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f181.google.com
Ironport-phdr: 9a23:A/rvkRBCPaQZI8NHgbKMUyQJP3N1i/DPJgcQr6AfoPdwSP3yocbcNUDSrc9gkEXOFd2CrakV1qyL7+igATVGusnR9ihaMdRlbFwst4Y/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbre9JomHxc+wzqW5/4DZSwROnju0J71oZl3ipgLI88ISnIFKK6AryxKPrGEeKMpMwmY9BFaWNAznruyx5oNn8j8Y7/Ml8sdaSuPxfr4lSb1DJDsjOmExosbssE+QHkO0+nIAXzBOwVJzCA/f4USiUw==

1) No 'assert' tactics with transparent result. (Maybe I don't know the right way.)

2) Opaque proofs where one needs transparency. :(

Require Import Omega.

Set Implicit Arguments.

Axiom PI: forall (P: Prop) (a b: P), a = b.

Structure bijection A B := {

bijF1: A -> B;

bijF2: B -> A;

_: forall x, bijF1 (bijF2 x) = x;

_: forall x, bijF2 (bijF1 x) = x

Definition fin n := { m | m < n }.

Definition finite A n := bijection A (fin n).

Example E1 a b (H: a <= b):

let A := { n | a <= n /\ n <= b }

in finite A (S b - a).

Proof.

intro A.

refine (let f := (_ : A -> fin (S b - a)) in _). Unshelve. all:swap 1 2.

intros [n [H1 H2]]. exists (n - a). intuition.

refine (let g := (_: fin (S b - a) -> A) in _). Unshelve. all:swap 1 2.

intros [n H0]. exists (n + a). intuition.

exists f g.

intros [n H0]. simpl. f_equal. (* apply PI. *)

Admitted.

[Coq-Club] Both annoying things in one place, Ilmārs Cīrulis, 03/13/2017
- Re: [Coq-Club] Both annoying things in one place, Ilmārs Cīrulis, 03/13/2017
- Re: [Coq-Club] Both annoying things in one place, Gaetan Gilbert, 03/13/2017
  - Re: [Coq-Club] Both annoying things in one place, Ilmārs Cīrulis, 03/13/2017