The Coq mailing list

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

Nice !

Thank you for those examples and remark about the automatic introduction of variables.

Have a nice day,

Fabian Pijcke

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

OK, I got confused myself as to which you were talking about.

Here are some more standard examples of custom inversion principles.
It does seem that, for some reason, inversion ? using ? doesn't
automatically do intros.

Inductive vector (A:Type) : nat -> Type :=
| vector_nil : vector A 0
| vector_cons : A -> forall {n:nat}, vector A n -> vector A (S n).

Arguments vector_nil [A].
Arguments vector_cons [A] h [n] t : rename.

Definition vector0_inv : forall {A:Type} (P : vector A 0 -> Type),
  P vector_nil -> forall v : vector A 0, P v :=
fun A P Pnil v =>
  match v in (vector _ n) return
    (match n return (vector A n -> Type) with
     | 0 => P
     | S _ => fun _ => unit
     end v) with
  | vector_nil => Pnil
  | vector_cons _ _ _ => tt
  end.

Definition vectorS_inv : forall {A:Type} {n:nat}
  (P : vector A (S n) -> Type),
  (forall (h:A) (t:vector A n), P (vector_cons h t)) ->
  forall v : vector A (S n), P v :=
fun A n P Pcons v =>
match v in (vector _ n) return
  (match n return (vector A n -> Type) with
   | 0 => fun _ => unit
   | S m => fun v => forall P : vector A (S m) -> Type,
       (forall (h:A) (t:vector A m), P (vector_cons h t)) -> P v
   end v) with
| vector_nil => tt
| vector_cons h m t => fun P' Pcons' => Pcons' h t
end P Pcons.

Definition vector_hd {A:Type} {n:nat} (v:vector A (S n)) : A.
(* for illustration only, do not actually define meaningful functions
   this way *)
inversion v using @vectorS_inv.
intros h t.
exact h.
Defined.

Definition vector_tl {A:Type} {n:nat} (v:vector A (S n)) : vector A n.
(* for illustration only, do not actually define meaningful functions
   this way *)
inversion v using @vectorS_inv.
intros h t.
exact t.
Defined.

Proposition vector_decomp : forall {A:Type} {n:nat}
  (v:vector A (S n)), vector_cons (vector_hd v) (vector_tl v) = v.
Proof.
intros.
inversion v using @vectorS_inv.
intros.
simpl.
reflexivity.
Qed.

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

Definition Fin0_inv (P : Fin 0 -> Type) :
  forall i : Fin 0, P i :=
fun i =>
match i in (Fin n) return
  (match n return (Fin n -> Type) with
   | 0 => P
   | S _ => fun _ => unit
   end i) with
| FinO _ => tt
| FinS _ _ => tt
end.

Definition FinS_inv {n:nat} (P : Fin (S n) -> Type) :
  P FinO -> (forall j : Fin n, P (FinS j)) ->
  forall i : Fin (S n), P i :=
fun P0 PS i =>
match i in (Fin n) return
  (match n return (Fin n -> Type) with
   | 0 => fun _ => unit
   | S m => fun i => forall P : Fin (S m) -> Type,
       P FinO -> (forall j : Fin m, P (FinS j)) -> P i
   end i) with
| FinO m => fun P' P0' PS' => P0'
| FinS m j => fun P' P0' PS' => PS' j
end P P0 PS.

Proposition Fin0_empty : notT (Fin 0).
Proof.
intro i.
inversion i using @Fin0_inv.
Qed.

Proposition FinS_decomp : forall {n:nat} (i : Fin (S n)),
  i = FinO \/ exists j, i = FinS j.
Proof.
intros.
inversion i using @FinS_inv.
+ left; reflexivity.
+ intro j. right; eexists; reflexivity.
Qed.
--
Daniel Schepler

On Wed, Jul 23, 2014 at 1:34 PM, shepi42 . <fabian.pijcke AT gmail.com> wrote:
> 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
>> >>
>> >
>
>