The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Would the tactic you're describing be able to handle cases like FinS i = FinS j where it requires multiple levels of "generalized return types"?  Here's an example of roughly how I'd picture an improved inversion/destruct tactic working in this case:

Inductive Fin : nat -> Set :=
| FinO {n} : Fin (S n)
| FinS {n} (i:Fin n) : Fin (S n).

Definition FinS_inj : forall {n:nat} (i j:Fin n),
  FinS i = FinS j -> i = j.
Proof.
intros.

(* we want to write
refine (match H in (_ = FinS_j) return ? with
| eq_refl => _
end).
Figure out what to put as the return type. *)

Definition return_type_1 (n:nat) (i:Fin n) (FinS_j:Fin (S n)) : Prop.
(* requirement: return_type_1 n i (FinS j) = (i = j) *)
revert i.  (* n in the type of i appears in the type of FinS_j *)

(* we want to write
refine (match FinS_j in (Fin S_n) return ? with
        | FinO => ?
        | FinS j => fun i => i = j
        end).
Figure out what to put as the return type. *)

Definition return_type_2 (S_n:nat) : Type.
(* requirement: return_type (S n) = Fin n -> Prop *)
exact (match S_n return Type with
       | 0 => unit
       | S n => Fin n -> Prop
       end).
Defined.

(* back in return_type_1, we're ready to go *)
exact (match FinS_j in (Fin S_n) return (return_type_2 S_n) with
       | FinO _ => fun _ => True
       | FinS n j => fun i => i = j
       end).
Defined.

(* back in FinS_inj, we're ready to go *)
refine (match H in (_ = FinS_j) return (return_type_1 n i FinS_j) with
        | eq_refl => _
        end).
unfold return_type_1.
reflexivity.
Qed.


(* And for a more complex example with dependent inversion of e : FinS i = FinS j *)
Lemma FinS_eq_surj : forall {n:nat} (i j:Fin n) (e : FinS i = FinS j),
  exists e':i=j, f_equal FinS e' = e.
Proof.
intros.

(* want to write
refine (match e in (_ = FinS_j) return ? with
        | eq_refl => _
        end).
Figure out what to put as the return type. *)

Definition return_type_1' (n:nat) (i:Fin n) (FinS_j:Fin (S n))
  (e:FinS i = FinS_j) : Prop.
(* Requirement: return_type_1' n i (FinS j) e = (exists e':i=j, f_equal FinS e' = e *)

revert i e. (* i because its type depends on n appearing in type of FinS_j,
               e because it's dependent on i. *)
(* want to write
refine (match FinS_j in (Fin S_n) return ? with
        | FinS n j => fun i e => exists e':i=j, f_equal FinS e' = e
        | FinO => ?
        end).
Figure out what to put as the return type. *)

Definition return_type_2' (S_n:nat) (FinS_j : Fin S_n) : Type.
(* Requirement: return_type_2' (S n) (FinS j) = (forall i:Fin n, FinS i = FinS_j -> Prop). *)
revert FinS_j.
exact (match S_n return (Fin S_n -> Type) with
       | S n => fun FinS_j => forall i:Fin n, FinS i = FinS_j -> Prop
       | O => fun _ => unit
       end).
Defined.

(* back in return_type_1', ready to go *)
exact (match FinS_j in (Fin S_n) return (return_type_2' S_n FinS_j) with
       | FinS n j => fun i e => exists e':i=j, f_equal FinS e' = e
       | FinO _ => fun _ _ => True
       end).
Defined.

(* back in FinS_eq_surj *)
refine (match e in (_ = FinS_j) return (return_type_1' n i FinS_j e) with
        | eq_refl => _
        end).
unfold return_type_1'.
exists eq_refl.
reflexivity.
Qed.
--

Daniel Schepler

On Fri, Oct 11, 2013 at 7:52 AM, gallais <guillaume.allais AT strath.ac.uk> wrote:

Hi all,

I thought I'd throw in a couple of references:

Jean-François Monin talked at the 2nd Coq Workshop about these proofs
by diagonalization in "Proof Trick: small Inversions":
http://coq.inria.fr/coq-workshop/2010

Pierre Boutillier and Thomas Braibant have been working on an automation
of this process. Here's a blog post about it and the github repository
with the implementation:
http://gallium.inria.fr/blog/a-new-Coq-tactic-for-inversion/
https://github.com/braibant/invert
As far as I know, this is destined to be integrated as part of Coq's
official codebase in a future release.

Cheers,

On 10/10/13 22:17, t x wrote:

Vincent, Robbert, Geoff: your examples are much more insightful.

I particularly like Robbert's example. It has just the right amount of
"generalizable to other cases" + "simple to understand."

Thanks!


On Thu, Oct 10, 2013 at 1:43 PM, Geoff Reedy <geoff AT programmer-monk.net>wrote:

On Thu, Oct 10, 2013 at 01:16:53PM -0700, t x said

Inductive Nat : Type :=
| O: Nat
| S: forall (n: Nat), Nat.

Lemma lem:
   O <> S O.
[...]
Is there a simpler proof of this?

I think this is as short as it gets:

eq_ind O (fun n => match n with O => True | S _ => False end) I (S O)