The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Apologies.
The last line before 'Admitted' has to be

    intros [n H0]. unfold f, g. simpl.
     replace (n + a - a) with n by intuition. f_equal. (* apply PI. *)
Admitted.

'replace' doesn't work here. 

On Mon, Mar 13, 2017 at 11:18 AM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

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.