# How do I define an induction principle for a type with a nested list of tuples?

I want to define an inductive type that describes records. The records are lists of elements, each element has a name and type. This requires nested recursion, so I've had to define an induction principle to handle it.

My problem is that I had to define a record as Record (names: list string) (types: list type_t) to make the induction principle work, when I'd really like it to be Record (elements: list (string * type_t))

Is there a way that I can do that?

Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Import ListNotations.

Inductive type_t : Type :=
| Integer
| Record (names: list string) (types: list type_t).

Section type_ind_strong.
Variable P : type_t -> Prop.
Hypothesis Integer_case :
P Integer.
Hypothesis Record_case :
forall (ns: list string) (ts: list type_t),
Forall P ts -> P (Record ns ts).
Fixpoint type_ind_strong (t : type_t) : P t :=
match t with
| Integer => Integer_case
| Record ns ts =>
Record_case ns ts
( ( fix type_list_ind (ts : list type_t) : Forall P ts :=
match ts with
| t :: ts' => Forall_cons t (type_ind_strong t) (type_list_ind ts')
| [] => Forall_nil _
end )
ts )
end.
End type_ind_strong.
$$$$

• I'm not sure I understand what you want the induction principle to look like. Concretely, what should happen if the lists are of different lengths? Commented May 2 at 10:20
• Why don't you just define the Record constructor of type_t as Record (types: list (string * type_t))? Commented May 2 at 15:35
• Yes, that is the problem. A list of tuples is the foolproof way to go about it. But it is that double nesting that I am finding tricky. Commented May 2 at 23:38

Concerning your question in a comment about Equal : _ -> _ -> Prop, this is how I would proceed, using an inductive predicate:

Require Import Coq.Lists.List.
Import ListNotations.

Section type_t.

Variable string : Type.

Unset Elimination Schemes.

Inductive type_t : Type :=
| Integer
| Record : list (string * type_t) -> type_t.

Set Elimination Schemes.

Section type_t_ind.

Variables (P : type_t -> Prop)
(HPI : P Integer)
(HPR : forall l, (forall x t, In (x,t) l -> P t) -> P (Record l)).

Fixpoint type_t_ind t : P t.
Proof.
destruct t as [ | l ].
+ apply HPI.
+ apply HPR.
induction l as [ | p l IHl ].
* intros _ _ [].
* intros x t [ E | H ].
- specialize (type_t_ind (snd p)); now subst.
- apply IHl with (1 := H).
Qed.

End type_t_ind.

Let sub_type_t s t :=
match t with
| Integer => False
| Record l => exists x, In (x,s) l
end.

Local Fact wf_sub_type : well_founded sub_type_t.
Proof. intros t; induction t; constructor; intros ? []; eauto. Qed.

Section type_t_rect.

Variables (P : type_t -> Type)
(HPI : P Integer)
(HPR : forall l, (forall x t, In (x,t) l -> P t) -> P (Record l)).

Theorem type_t_rect t : P t.
Proof.
induction t as [ [ | l ] IH ] using (well_founded_induction_type wf_sub_type).
+ apply HPI.
+ apply HPR.
intros x ? ?; apply IH; now exists x.
Qed.

End type_t_rect.

Definition type_t_rec (P : _ -> Set) := type_t_rect P.

Variable string_equal : string -> string -> Prop.

Inductive type_t_equal : type_t -> type_t -> Prop :=
| type_t_equal_I : type_t_equal Integer Integer
| type_t_equal_R l m : Forall2 string_equal (map fst l) (map fst m)
-> Forall2 type_t_equal (map snd l) (map snd m)
-> type_t_equal (Record l) (Record m)
.

Fact Forall2_refl X R l : (forall x : X, In x l -> R x x) -> Forall2 R l l.
Proof.
rewrite <- Forall_forall.
induction 1; auto.
Qed.

Hypothesis string_equal_refl : forall x : string, string_equal x x.

Fact type_t_equal_refl t : type_t_equal t t.
Proof.
induction t as [ | l IHl ]; constructor.
+ apply Forall2_refl; intros; apply string_equal_refl.
+ apply Forall2_refl.
intros ? ((x,t) & <- & ?)%in_map_iff; simpl; eauto.
Qed.

End type_t.
$$$$

• Great! Thanks! I think this will get me a long way. I particularly like how you didn't use a nested anonymous fix function in type_t_equal, and instead used Forall2 propositions that follow the structure of the inductive type more closely. It's less complex and easier to see what's happening. Commented May 5 at 8:35
• Notice that it is a nested inductive and I had to split Forall2 in half because of the strict positivity criteria. Commented May 5 at 12:30
• How does intros ? ((x,t) & <- & ?)%in_map_iff work? Commented May 6 at 8:59
• the %in_map_iff applies in_map_iff to the introduced hypothesis and then the ((x,t) & <- & ?) intro pattern is applied to this transformed hypothesis. This in much shorter than intros ? H; apply in_map_iff in H; destruct H as ((x,t) & <- & ?). Commented May 6 at 10:34
• Ah, thanks. It looked very useful, but I couldn't replicate the effect with the simpler Coq I knew. (I made good progress with what you gave me yesterday, I added references, arrays and procedures to type_t, which is almost everything I need.) Commented May 6 at 23:34

The question of recursors for types nested with lists, aka rose trees, is popping up quite often these days. I did develop a Coq library specifically for the purpose of dealing with these data structures and it is called Kruskal-Trees available on Github but also via opam.

Anyway, tailored to your specific data-structure, one can derive the following induction principle available uniformly in Type, Set and Prop bounded versions.

Require Import Coq.Lists.List.
Import ListNotations.

Section type_t.

Variable string : Type.

Unset Elimination Schemes.

Inductive type_t : Type :=
| Integer
| Record : list (string * type_t) -> type_t.

Set Elimination Schemes.

Section type_t_ind.

Variables (P : type_t -> Prop)
(HPI : P Integer)
(HPR : forall l, (forall x t, In (x,t) l -> P t) -> P (Record l)).

Fixpoint type_t_ind t : P t.
Proof.
destruct t as [ | l ].
+ apply HPI.
+ apply HPR.
induction l as [ | p l IHl ].
* intros _ _ [].
* intros x t [ E | H ].
- specialize (type_t_ind (snd p)); now subst.
- apply IHl with (1 := H).
Qed.

End type_t_ind.

Let sub_type_t s t :=
match t with
| Integer => False
| Record l => exists x, In (x,s) l
end.

Local Fact wf_sub_type : well_founded sub_type_t.
Proof. intros t; induction t; constructor; intros ? []; eauto. Qed.

Section type_t_rect.

Variables (P : type_t -> Type)
(HPI : P Integer)
(HPR : forall l, (forall x t, In (x,t) l -> P t) -> P (Record l)).

Theorem type_t_rect t : P t.
Proof.
induction t as [ [ | l ] IH ] using (well_founded_induction_type wf_sub_type).
+ apply HPI.
+ apply HPR.
intros x ? ?; apply IH; now exists x.
Qed.

End type_t_rect.

Definition type_t_rec (P : _ -> Set) := type_t_rect P.

End type_t.


If you need the fixpoints equations for your recursors, one should be a little more careful with their proofs but it is possible to prove these as well.

• Thank you. If I want to define a proposition for equality and prove that is reflexive ("Fixpoint Equal (t1 t2 : type_t) : Prop" and "Theorem Equal_reflexive : forall (t : type_t), Equal t t."), how would I use these go about that? Commented May 2 at 23:36
• What is the point of defining Equal in Prop ? There is already the polymorphic identity type @eq type_t also denoted _ = _, which is reflexive by its very definition. Maybe you want Equal as a test procedure, but then the output should be in bool, not Prop. Commented May 3 at 8:47
• I am trying to define a simple type system, which will include records. I started with Equal, but I'll want to do variations on that, like assignment compatibility. I defined Equal using a nested anonymous fix, but when I try to prove Equal_reflexive using your 'type_t_ind' I don't seem to get an inductive goal I can use for Equal (Record l) (Record l). I can do it with the type_ind_strong I defined, but maybe that was because it has close to the same structure. Commented May 4 at 0:05
• I am adding a new answer to explain how I would proceed Commented May 5 at 6:23
From Coq Require Import String List.
Import ListNotations.

(* Lift predicates through type constructors *)

Definition onSnd {A B : Type} (P : B -> Prop) (xy : A * B) : Prop :=
P (snd xy).

Definition onSndP {A B : Type} {P : B -> Prop} (allP : forall b : B, P b) (xy : A * B) : onSnd P xy
:= allP (snd xy).

Definition listForallP {A : Type} {P : A -> Prop} (allP : forall a : A, P a)
: forall xs : list A, List.Forall P xs :=
fix f (xs : list A) : List.Forall P xs :=
match xs with
| nil => Forall_nil P
| cons x xs => Forall_cons x (allP x) (f xs)
end.

(* Induction principle for very nested type *)

Unset Elimination Schemes. (* don't derive type_t_ind *)

Inductive type_t : Type :=
| Integer
| Record (elements : list (string * type_t)).

Fixpoint type_t_ind (P : type_t -> Prop)
(P_Integer : P Integer)
(P_Record : forall elements, List.Forall (onSnd P) elements -> P (Record elements))
(t : type_t) : P t :=
match t with
| Integer => P_Integer
| Record elements => P_Record elements (listForallP (onSndP (type_t_ind P P_Integer P_Record)) elements)
end.
$$$$

• Thank you. If I want to define a proposition for equality and prove that is reflexive ("Fixpoint Equal (t1 t2 : type_t) : Prop" and "Theorem Equal_reflexive : forall (t : type_t), Equal t t."), how would I use these go about that? Commented May 2 at 23:36
• you can do induction t. or induction t using my_type_t_ind. if you've given a different name to your induction principle. Commented May 3 at 7:18
• I defined Equal using a nested anonymous fix (which feels messy, but apparently the only way to do it). Using induction using you princle gives me the goals elements : list (string * type_t) and H : Forall (onSnd (fun t : type_t => Equal t t)) elements to prove Equal (Record elements) (Record elements), and I'm not sure where to go from there. Unfolding Equal gives me the fix function, which I can't work out what to do with. Commented May 4 at 0:02
• One approach is to define auxiliary lemmas that let you "remove" constructors from the goal. Find a relation R such that R e e' -> Equal (Record e) (Record e'). Commented May 4 at 6:14

Allow me to give a “these are not the droids you're looking for” answer.

A record is a mapping from field labels to corresponding values. A list of pairs, such as the one you are using, is not a mapping. It only represents one and is setting up some traps. What happens if the same field is repeated several times? Does the order of fields matter? Did you think about how the list membership predicate In used in the induction principle interacts with repeated fields?

These are all complications that go away once we use maps directly:

Inductive type_t : Type :=
| Integer
| Record (label : Type) : (label -> type_t) -> type_t.

Check type_t_rect.

(* type_t_rect
: forall P : type_t -> Type,
P Integer ->
(forall (label : Type) (t : label -> type_t),
(forall l : label, P (t l)) -> P (Record label t)) ->
forall t : type_t, P t
*)


The induction principle generated by Coq looks good to me. Now of course we could complain that label need not be finite etc. That is of course true, and such finiteness can be enforced if necesary, but is often needed only in small amounts that can be handled separately. And also, if you really want to use lists of strings, you can just specialize label to a finite type of strings.

• Yep the induction principle will be good here because this functional type_t is not nested. But on the other hand, it is not a datatype: no decidable equality, no finiteness property (as you said) even if you bound the allowable labels. All because the function type _ -> type_t is neither decidable nor listable (unless FunExt). Commented May 3 at 12:56
• @DominiqueLarchey-Wendling: of course you have a point. But are you really sure you need decidable equality? What are you doing with your records, precisely? Commented May 3 at 18:31
• Thank you. I'm trying to describe the type system of a simple Pascal or C like language. So, for records the order is significant, and I'd need to be able to extract lists of element names, which I don't think would be possible if I use a function. Commented May 3 at 23:36
• C does not have structural comparison of stucts, so the order is not significant because you are never asked whethere the types {foo : int ; bar : bool} and {bar : bool; foo : int}` are equal. Or do you have structural type equality rules? Or a compiler which must respect the ordering of the fields? Commented May 4 at 9:14