The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

>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.

Require Import Omega.
Set Implicit Arguments.

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).

Lemma exist_irr {A:Type} (P:A->Prop) (H : forall x (y y' : P x), y = y')
  : forall x x' y y', x = x' -> exist P x y = exist P x' y'.
Proof.
  intros x x' y y' e;destruct e;f_equal;apply H.
Qed.

Example E1 a b (H: a <= b):
  let A := { n | a <= n /\ n <= b }
  in finite A (S b - a).
Proof.
  intro A.
  simple refine (let f := (_ : A -> fin (S b - a)) in _).
    intros [n [H1 H2]]. exists (n - a). intuition.
  simple refine (let g := (_: fin (S b - a) -> A) in _).
    intros [n H0]. exists (n + a). intuition.
  exists f g.
  intros [n H0]. simpl.
  apply exist_irr;intuition. apply le_unique.
  intros [n [H0 H1]]. simpl.
  apply exist_irr;intuition.
  destruct y,y';f_equal;apply le_unique.
Defined.