The Coq mailing list

["shepi42 ." <fabian.pijcke AT gmail.com>]

By the way, it seems that the inversion ... using ... form is hardly used in practice.

I couldn't find any occurence in the coq standard library nor in the CoRN library.

Is there a reason for that ? Maybe lemmas of the form type -> case1 \/ case2 \/ case3 are preferred ?

Fabian Pijcke

2014-07-23 22:34 GMT+02:00 shepi42 . <fabian.pijcke AT gmail.com>:

Hello !

Thank you for your answer, but again, I'm interested in inversion principle and not induction.

Maybe I miss something, and the two concepts are the same, could you confirm it ? :s

Fabian Pijcke

2014-07-23 21:59 GMT+02:00 Daniel Schepler <dschepler AT gmail.com>:

Here's a silly example of defining a custom induction principle and
using it.  Note that the form of T0_ind itself excludes the impossible
Tbase case, and similarly the form of TS_ind excludes the impossible
T0 case.

Inductive T : nat -> Set :=
| T0 : T 0
| Tbase {n} : T n -> T (S n)
| Tstep {n} : T n -> T n.

Lemma T0_ind : forall (P : T 0 -> Prop),
  P T0 -> (forall x : T 0, P x -> P (Tstep x)) ->
  forall x : T 0, P x.
Proof.
intros P P0 Pstep.
cut (forall (n:nat) (y:T n), match n return (T n -> Prop) with
                             | 0 => P
                             | S _ => fun _ => True
                             end y).
+ intro. apply H.
+ induction y; auto.
  destruct n; auto.
Qed.

Fixpoint T0_of_nat (n:nat) : T 0 :=
match n with
| 0 => T0
| S m => Tstep (T0_of_nat m)
end.

Lemma T0_of_nat_surj : forall x : T 0, exists n:nat, x = T0_of_nat n.
Proof.
induction x using T0_ind.
+ exists 0; reflexivity.
+ destruct IHx as [n]. exists (S n). simpl. f_equal; trivial.
Qed.

Lemma TS_ind : forall {n:nat} (P : T (S n) -> Prop),
  (forall y : T n, P (Tbase y)) ->
  (forall x : T (S n), P x -> P (Tstep x)) ->
  forall x : T (S n), P x.
Proof.
intros n P Pbase Pstep x.
cut (forall (n:nat) (y:T n),
     match n return (T n -> Prop) with
     | 0 => fun _ => True
     | S m => fun x => forall P : T (S m) -> Prop,
                (forall y : T m, P (Tbase y)) ->
                (forall y : T (S m), P y -> P (Tstep y)) ->
                P x
     end y).
+ intros. exact (H (S n) x P Pbase Pstep).
+ clear P Pbase Pstep. induction y; auto.
  destruct n0; auto.
  intros. apply IHy; auto.
Qed.

Fixpoint TS_maker {n:nat} (x : T n) (m : nat) : T (S n) :=
match m with
| 0 => Tbase x
| S m' => Tstep (TS_maker x m')
end.

Lemma TS_maker_surj : forall (n:nat) (y : T (S n)),
  exists (x : T n) (m : nat), y = TS_maker x m.
Proof.
intros.
induction y using TS_ind.
+ exists y; exists 0; reflexivity.
+ destruct IHy as [x [m ?]]. exists x; exists (S m); simpl.
  f_equal; trivial.
Qed.
--
Daniel Schepler

On Wed, Jul 23, 2014 at 12:11 PM, shepi42 . <fabian.pijcke AT gmail.com> wrote:
> Aww I'm sorry, I implemented my own _induction_ principle this morning, and
> I went wrong speaking about induction instead of inversion.
>
> If I'm right, Print ind_nat prints out the induction principle generated by
> default, so my (real) question is "is there an equivalent command to print
> the inversion principle generated by default ?"
>
> I've seen something like "Derive Inversion_clear", but I don't really get
> how this works and I'm not sure it correspond to the default inversion
> principle, especially, it seems trivially false cases are not wiped out.
>
> Thank you for your answer anyway, just slap me twice if the inversion and
> induction principles use the same definition in definitive :p
>
> Fabian Pijcke
>
>
> 2014-07-23 20:19 GMT+02:00 Jonathan <jonikelee AT gmail.com>:
>
>> On 07/23/2014 02:15 PM, Fabian Pijcke wrote:
>>>
>>> Dear list,
>>>
>>> I use the tactic "inversion H using myinversionprinciple.".
>>>
>>> However, the principle I come with has several flaws. For example, it
>>> does not
>>> introduce new variables automatically, and doesn't skip the trivially
>>> false
>>> cases.
>>>
>>> Is there a way to Check the default induction principle used for an
>>> Inductive
>>> type ?
>>
>>
>> You mean, just to examine an existing one to see how it is defined? Try:
>> Print nat_ind.
>>
>> -- Jonathan
>>
>