Ssreflect Users Discussion List

[Ian Zimmerman <>]

Ok, here's my next stumbling block.  My entire file until now:

>> begin quote

From mathcomp Require Import ssreflect ssrfun ssrbool.
Require Import FunctionalExtensionality.
Require Import ClassicalEpsilon.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require Import Utf8.

Section Transformations.

Variable T: Type.

Let I := @id T.

Lemma id_cancel: cancel I I.
Proof.
  exact.
Qed.

Let bij_id_witness := Bijective id_cancel id_cancel: bijective I.

Lemma bij_id: bijective I.
Proof.
  exact: bij_id_witness.
Qed.

Let has_invimg (f: T → T) (y: T) := ∃ x: T, f x = y.

Lemma img_has_invimg: ∀ f: T → T, ∀ x: T, has_invimg f (f x).
Proof.
  rewrite /has_invimg => f x; exists x; reflexivity.
Qed.

Let is_preimg (f: T → T) (y: T) := λ x: T, has_invimg f y → f x = y.

Let eps_preimg (f: T → T) (y: T) := epsilon (inhabits y) (is_preimg f y).

Lemma has_preimg: ∀ f: T → T, ∀ y: T, ∃ x: T, is_preimg f y x.
Proof.
  move => f y; set INVfy := has_invimg f y.
  have: {INVfy} + {¬ INVfy} by apply: excluded_middle_informative.
  case; [firstorder ..].
Qed.

Lemma inj_eps_is_preimg: ∀ f: T → T, ∀ y: T, injective f → is_preimg f y 
(eps_preimg f y).
Proof.
  move => f y INJf; apply: epsilon_spec; exact: has_preimg.
Qed.

Lemma inj_preimg_cancels: ∀ f: T → T, injective f → cancel f (eps_preimg f).
Proof.
  move => f INJf x; set y := f x; set x' := eps_preimg f y.
  have: is_preimg f y x' by apply: inj_eps_is_preimg.
  rewrite /is_preimg.
  have: has_invimg f y by apply: img_has_invimg.
  firstorder.
Qed.

Lemma inj_r_inv: ∀ f: T → T, injective f → ∃ f', cancel f f'.
Proof.
  move => f INJf; exists (eps_preimg f); apply: inj_preimg_cancels INJf.
Qed.

Lemma bij_r_inv: ∀ f: T → T, bijective f → ∃ f', cancel f f'.
Proof.
  move => f BJf; have: injective f by [apply: bij_inj BJf]; apply inj_r_inv.
Qed.

Lemma bij_r_inv_unique: ∀ f f' f'': T → T, bijective f  → cancel f f' → 
cancel f f'' → f' = f''.
Proof.
  move => f f' f'' BJf Cf' Cf''; extensionality y; move: BJf f' f'' Cf' Cf'' 
y.
  exact: bij_can_eq.
Qed.

Proposition bij_r_inv_l_inv: ∀ f f': T → T, bijective f → cancel f f' → 
cancel f' f.
Proof.
  move => f f' BJf.
  have: ∀ g, cancel f f' → cancel f g → f' = g.
  - move => g CANff' CANfg; apply: bij_r_inv_unique BJf CANff' CANfg.
  case: BJf => g CANfg CANgf UNIQf' CANff'.
  have: f' = g by apply: UNIQf' g CANff' CANfg.
  move => EQgf'. move: EQgf' CANgf.

>> end quote

And here I am left with this goalstack:

f, f', g : T → T
CANfg : cancel f g
UNIQf' : ∀ g : T → T, cancel f f' → cancel f g → f' = g
CANff' : cancel f f'
______________________________________(1/1)
f' = g → cancel g f → cancel f' f

Sure seems like first order to me ... but not to Coq:

Ltac call to "firstorder (tactic_opt) (firstorder_using)" failed.
Tactic failure: reversible in 1st order mode.

So what's going on here, and how can I proceed?

Another question: I wish the last apply step would remove the hypotheses
is uses from the context, but it doesn't, and something like the
following which _should_ have that effect according to the doc, doesn't
work either:

have: f' = g by apply: UNIQf' g CANff' CANfg => {UNIQf' CANff' CANfg}

In general, the doc is tough to read because information on most tactics
is not in one place :-(

-- 
Please don't Cc: me privately on mailing lists and Usenet,
if you also post the followup to the list or newsgroup.
To reply privately _only_ on Usenet and on broken lists
which rewrite From, fetch the TXT record for no-use.mooo.com.