Hello!
Summary: I’m defining my own induction principle for inductively defined types which use the standard library list in their definitions. I’ve encountered a problem: it seems that I need to define a new induction principle for each of the types in the mutually defined set even though their contents are essentially identical. Is there a better way to define mutual induction principles manually or is repetition in my code the price I pay for satisfying the fixpoint checker?
Detail: I’ll provide a concrete example. For my question, I’ll use the types a and b defined as so:
Require Import Bool.
Require Import List. Import ListNotations.
Inductive a := A1 : a | A2 : b -> a
with b := B1 : b | B2 : list a -> b.
I can’t use Scheme to generate a mutual induction principle for these types as the presence of list, which is not defined in the Inductive declaration, prevents me from getting the inductive properties of a terms within the constructor B2. So I need to define my own, which I do as follows:
Definition a_ind'' :
forall
(PA : a -> Prop)
(PB : b -> Prop)
(PListA : list a -> Prop),
PA A1 ->
(forall y : b, PB y -> PA (A2 y)) ->
PB B1 ->
(forall xs : list a, PListA xs -> PB (B2 xs)) ->
PListA [] ->
(forall (x : a), PA x -> forall (xs : list a), PListA xs ->
PListA (x :: xs)) ->
forall x : a, PA x
:=
fun
(PA : a -> Prop)
(PB : b -> Prop)
(PListA : list a -> Prop)
(pA1 : PA A1)
(pA2 : forall y : b, PB y -> PA (A2 y))
(pB1 : PB B1)
(pB2 : forall xs : list a, PListA xs -> PB (B2 xs))
(pANil : PListA [])
(pACons : forall (x : a), PA x -> forall (xs : list a), PListA xs ->
PListA (x :: xs))
=>
fix FA (x : a) : PA x :=
match x as x' return (PA x') with
| A1 => pA1
| A2 y => pA2 y (FB y)
end
with FB (y : b) : PB y :=
match y as y' return (PB y') with
| B1 => pB1
| B2 xs =>
let FListA :=
fix FListA (xs : list a) : PListA xs :=
match xs as xs' return (PListA xs') with
| [] => pANil
| x::xs' =>
pACons x (FA x) xs' (FListA xs')
end
in
pB2 xs (FListA xs)
end
for
FA
.
As verbose and crude as this is, it gets the job done. I can now prove simple theorems on type a. For instance, given boolean equality function on these types…
Fixpoint a_eqb (x1 x2 : a) : bool :=
match x1, x2 with
| A1, A1 => true
| A2 y1, A2 y2 => b_eqb y1 y2
| _, _ => false
end
with b_eqb (y1 y2 : b) : bool :=
match y1, y2 with
| B1, B1 => true
| B2 xs1, B2 xs2 =>
let fix list_a_eqb (xs1 xs2 : list a) : bool :=
match xs1, xs2 with
| nil, nil => true
| x1::xs1', x2::xs2' => a_eqb x1 x2 && list_a_eqb xs1' xs2'
| _, _ => false
end
in
list_a_eqb xs1 xs2
| _, _ => false
end
.
…I can prove reflexivity of boolean equality.
Fixpoint list_a_eqb (xs1 xs2 : list a) : bool :=
match xs1, xs2 with
| nil, nil => true
| x1::xs1', x2::xs2' => a_eqb x1 x2 && list_a_eqb xs1' xs2'
| _, _ => false
end
.
Lemma a_eqb_refl : forall (x : a), a_eqb x x = true.
Proof.
induction x using a_ind'' with
(PB := fun (y : b) => b_eqb y y = true)
(PListA := fun (xs : list a) => list_a_eqb xs xs = true).
- simpl; reflexivity.
- simpl; exact IHx.
- simpl; reflexivity.
- induction xs as [|x xs']. reflexivity.
simpl in IHx. apply andb_true_iff in IHx. destruct IHx as [IHx IH'].
simpl. apply andb_true_iff. split. apply IHx. exact IH'.
- simpl. reflexivity.
- simpl. apply andb_true_iff. split. apply IHx. exact IHx0.
Qed.
This is all well and good (modulo my naivete with respect to good practice). But if I want to prove similar things about b, I need an appropriate induction principle for it. Since the fix expression in a_ind'' can only produce one of the mutually defined functions, I have no way of exposing both FA and FB in that definition. As far as I can tell, I’m stuck writing a second induction principle:
Definition b_ind'' :
forall
(PB : b -> Prop)
(PA : a -> Prop)
(PListA : list a -> Prop),
PA A1 ->
(forall y : b, PB y -> PA (A2 y)) ->
PB B1 ->
(forall xs : list a, PListA xs -> PB (B2 xs)) ->
PListA [] ->
(forall (x : a), PA x -> forall (xs : list a), PListA xs ->
PListA (x :: xs)) ->
forall y : b, PB y
:=
fun
(PB : b -> Prop)
(PA : a -> Prop)
(PListA : list a -> Prop)
(pA1 : PA A1)
(pA2 : forall y : b, PB y -> PA (A2 y))
(pB1 : PB B1)
(pB2 : forall xs : list a, PListA xs -> PB (B2 xs))
(pANil : PListA [])
(pACons : forall (x : a), PA x -> forall (xs : list a), PListA xs ->
PListA (x :: xs))
=>
fix FA (x : a) : PA x :=
match x as x' return (PA x') with
| A1 => pA1
| A2 y => pA2 y (FB y)
end
with FB (y : b) : PB y :=
match y as y' return (PB y') with
| B1 => pB1
| B2 xs =>
let FListA :=
fix FListA (xs : list a) : PListA xs :=
match xs as xs' return (PListA xs') with
| [] => pANil
| x::xs' =>
pACons x (FA x) xs' (FListA xs')
end
in
pB2 xs (FListA xs)
end
for
FB
.
This is nearly identical to the first except that the PB proposition comes first and FB is the overall result. I can then use b_ind'' in proofs if I want. But this feels silly, especially since mutually inductive types which use lists in their definition seem (to me, at least) not to be uncommon, so I’d expect that people run into this often enough that a better solution exists. What should I be doing instead?
btw, I’m aware that, in this case, I could prove reflexivity of b’s boolean equality by manually unwrapping a layer rather than rewriting the whole proof:
Lemma list_a_eqb_refl : forall (xs : list a), list_a_eqb xs xs = true.
Proof.
induction xs. { simpl. reflexivity. }
simpl. apply andb_true_iff. split. apply a_eqb_refl. exact IHxs.
Qed.
Lemma b_eqb_refl : forall (y : b), b_eqb y y = true.
Proof.
destruct y. { simpl. reflexivity. }
simpl. apply list_a_eqb_refl'.
Qed.
I’m trying to avoid this “solution” because my real problem involves more complex propositions and I’d prefer not to have to write them all from the perspective of a single type.
Thanks for reading! 