The Coq mailing list

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

Big thank you, Gaëtan!

On Mon, Mar 13, 2017 at 11:41 AM, Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr> wrote:

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

You can use [simple refine (let x := _ : A in _)] instead of [refine. Unshelve. swap.]

See https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v#L856 to make it into a [transparent assert] tactic.

>2) Opaque proofs where one needs transparency. :(

le_unique from Arith is enough for this proof.

Gaëtan Gilbert

On 13/03/2017 10:18, Ilmārs Cīrulis 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.