It is one of those long questiosn,

So I am doing basic proof of conflunce by Tait-martinlof approach, and I am stuck somewhere when dealing the lemma that says:

```
Σ ⊢ t ⇒ t' ->
Σ ⊢ t ⟶* t'
```

The idea I followed (which worked so far until inductive types) was to utiize helper inversion principles for multi step reduction, (I call them transitivity lemmas)

One example of those lemmas is the following:

```
Σ ⊢ m ⟶* m' ->
Σ ⊢ n ⟶* n' ->
Σ ⊢ appl m n ⟶* appl m' n'.
```

Additional non standard notation is the following:

`Σ ⊢ x [⇒] y`

where x and y are list of terms, and this is basically `forall ts, PIn ts (zip x y) -> Σ ⊢ fst ts ⇒ snd ts`

. Like wise we have `Σ ⊢ x [⟶*] y`

They are useful because the way recursors are defined.

Anyways, Inductive types are defined as following:

```
Inductive Term : Type
....
| induct (n: string)
(* constructor for inductive types *)
| constr (n: string)
(* Recursor à la Peter Dybjer & Martin Lof *)
| rec
(* name of the inductive type we are recursing on *)
(n: string)
(params: seq Term)
(* output type of the recursion branch *)
(C: Term)
(* what do to for every constructor*)
(branches: seq Term)
(* the main argumen to provide to the recursor function *)
(arg: Term).
```

`Induct`

and `constr`

refers to names that are part of global context where hte real inductive types lives I simply followed coq. I only mention them for sake of completeness

I define the single step reduction for `rec`

as following:

```
Reserved Notation "Σ '⊢' x '⟶' y" (at level 20, x at next level, y at next level).
Inductive Reduction: Module -> Term -> Term -> Prop :=
....
| Reduction_recp: forall Σ n p c b a p' s t l1 l2,
Σ ⊢ s⟶t ->
p = l1 ++ s::l2 ->
p' = l1 ++ t::l2 ->
Σ ⊢ rec n p c b a ⟶ rec n p' c b a
| Reduction_recc: forall Σ n p c b a c',
Σ ⊢ c ⟶ c' ->
Σ ⊢ rec n p c b a ⟶ rec n p c' b a
| Reduction_recb: forall Σ n p c b a b' s t l1 l2,
Σ ⊢ s⟶t ->
b = l1 ++ s::l2 ->
b' = l1 ++ t::l2 ->
Σ ⊢ rec n p c b a ⟶ rec n p c b' a
| Reduction_reca: forall Σ n p c b a a',
Σ ⊢ a ⟶ a' ->
Σ ⊢ rec n p c b a ⟶ rec n p c b a'
| Reduction_rec_beta: forall Σ n p c b a induct_body cname cidx branch args ctype args_types,
mod_get Σ n = Some (module_inductive n induct_body) ->
split_appl a = (constr cname, args) ->
induct_get_constr_idx induct_body cname = Some cidx ->
nth_error b cidx = Some branch ->
induct_get_constr_type induct_body cname = Some ctype ->
snd (split_pi ctype) = args_types ->
Σ ⊢ rec n p c b a ⟶ combine_branch_args branch args args_types n p c b
where "Σ '⊢' t1 '⟶' t2" := (Reduction Σ t1 t2).
```

For sake of discussion `Reduction_rec_beta`

might not be important, but it really retrieves everything from the global context.

Now the transitivity lemma for recursors says the following:

```
Σ ⊢ c ⟶* c' ->
Σ ⊢ a ⟶* a' ->
length p = length p' ->
Σ ⊢ p [⟶*] p' ->
length b = length b' ->
Σ ⊢ b [⟶*] b' ->
Σ ⊢ rec n p c b a ⟶* rec n p' c' b' a'.
```

I do things by induction on `⟶*`

and for the lists I do induction on the lists themselves and discharge the trivial cases.

But there is always case like the following where I need to prove:

```
size b = size b' ->
Σ ⊢ b [⟶*] b' ->
Σ ⊢ rec n p c b a ⟶* rec n p c b' a.
```

Trivial induction on `b`

would give an interesting case where The goal is:

```
Σ ⊢ rec n p c b a ⟶* rec n p c b' a
Σ ⊢ rec n p c (b1' :: b) a ⟶* rec n p c (b1' :: b') a
```

The problem here is that there is no way to to get rid of `b1'`

(and it shouldn't be doable anyways because that then recursion will not be well typed ... that does not matter for purposes of reduction)

and I am stuck, I know why I am stuck, at least the immediate reason, because the way things are structured treats arrays or branches, or arguments are a whole one thing, but I feel blocked and don't know what to try next to get around this issue.

I guess you need to show that if `Σ ⊢ b [⟶*] b'`

then there is a list `b1 ... bn`

such that b = b1, b' = bn and for all i < n, `bi = bi_0 ++ xi ++ bi_1`

, `bi+1 = bi_0 ++ yi ++ bi_1`

and `xi ⟶* yi`

ie reduce on 1 branch at a time

So I am not quite sure how will I use it, I thought it might be clear after I implement it but is still not:

my version looks like the following:

```
forall b b' Σ:
size b = size b' ->
Σ ⊢ b [⟶*] b' ->
exists bs, (* the list is b::bs *)
last b bs = b' /\
forall i b1 b2,
nth_error (b::bs) i = Some b1 ->
nth_error (b::bs) (S i) = Some b2 ->
exists bl br t t',
b1 = bl ++ t::br /\
b2 = bl ++ t'::br /\
Σ ⊢ t ⟶* t'.
```

And I cannot see how can I use it here:

```
Hlen: length b = length b'
Hpred: Σ ⊢ b [⟶*] b'
================== Goal
Σ ⊢ rec n [::] c b a ⟶* rec n [::] c b' a
```

I am thinking about a slightly different version

```
forall b b' Σ:
size b = size b' ->
Σ ⊢ b [⟶*] b' ->
exists bs, (* the list is b::bs *)
last b bs = b' /\
forall i b1 b2,
nth_error (b::bs) i = Some b1 ->
nth_error (b::bs) (S i) = Some b2 ->
exists bl br t t',
b1 = bl ++ t::br /\
b2 = bl ++ t'::br /\
Σ ⊢ t ⟶ t'. (*note this is single step*)
```

And I think I can use it to convert `[-->*]`

to array of single step reductions. I am still not sure how helpful would that be, so I wanted to ask you about what you had in mind?

Also how did you come up with this idea ? is this a known pattern ?

apply the lemma on Hpred, destruct the exists, you get `bs, H : last b bs = b' /\ ... |- rec b ->* rec b'`

`induction bs`

should then give 2 cases

- bs = [], this gives
`last b [] = b'`

ie`b = b'`

so goal solved by reflexivity `bs = b1 :: bs'`

, if`bs'`

is empty then`b1 = b'`

and you use congruence for`rec`

if`bs'`

nonempty then`last b bs' = last b (b1 :: bs') = b'`

and you have a transitivity step

you can use single step in the lemma, or you can prove congruence for -->* (ie Reduction_recb but using -->*)

do as you prefer there

BTW is the length b = length b' hypothesis really necessary? It seems like it should be implied by [-->*]

BTW is the length b = length b' hypothesis really necessary? It seems like it should be implied by [-->*]

not in my case, it is a definition that looks like this):

```
(R : A -> B -> Prop): (forall ts, PIn ts (zip s1 s2) -> R ts.1 ts.2)
```

Where R is the multi step reduction relation

I might need to use something like:

```
Inductive SeqForallPair {A B} (R: A -> B -> Prop) : seq A -> seq B -> Prop :=
| SeqForallPair_empty: SeqForallPair R [::] [::]
| SeqForallPair_cons a b sa sb: R a b -> SeqForallPair R sa sb -> SeqForallPair R (a::sa) (b::sb).
```

But I will do that later when the need arises.

Edit: if I recall correctly, it breaks some strict positivity requirements in reduction and I do't want to have to write induction principles by hand again for nested induction, but I am open to ideas

I guess zip does some nonsense when the lists don't have the same size

maybe it would make sense to add the length constraint inside [-->*]

anyway this is just a nitpick feel free to ignore

I am intending to clean things up once I finish the proof through .. the proof of confluence. but I wanted to ask you how did you figure out this solution, is it a known pattern for particular problems ? the way you describe the solution makes me feel like you saw this particular problem before.

I looked at the constructors you gave for --> and tried to figure out how [-->*] could be expressed in a way compatible with them

quick question does this idea of list of reduction steps have anything to do with the concept of "step indexing" which unfortunately don't know yet? or are they totally unrelated ?

unrelated

or, I'd say mostly unrelated but... step-indexing lets you use _fuel_ to define propositions

and when reasoning about programs, if `e -> e'`

, you typically have one less fuel unit when talking about `e'`

.

not sure if that helps or not, but all existing uses have languages with deterministic call-by-value reduction, so questions about confluence don't even apply

yeah probably not realted at all, I was thinking of good name for the lemma that decompose the list of multi steps to single steps and the name step index popped to mind. funny thing my half knowledge of everything.

But thanks alot.

one can't be an expert in everything :-)

also proving this:

```
forall b b' Σ:
size b = size b' ->
Σ ⊢ b [⟶*] b' ->
exists bs, (* the list is b::bs *)
last b bs = b' /\
forall i b1 b2,
nth_error (b::bs) i = Some b1 ->
nth_error (b::bs) (S i) = Some b2 ->
exists bl br t t',
b1 = bl ++ t::br /\
b2 = bl ++ t'::br /\
Σ ⊢ t ⟶* t'.
```

is trivial but proving this

```
forall b b' Σ:
size b = size b' ->
Σ ⊢ b [⟶*] b' ->
exists bs, (* the list is b::bs *)
last b bs = b' /\
forall i b1 b2,
nth_error (b::bs) i = Some b1 ->
nth_error (b::bs) (S i) = Some b2 ->
exists bl br t t',
b1 = bl ++ t::br /\
b2 = bl ++ t'::br /\
Σ ⊢ t ⟶ t'.
```

without the last `-->*`

is not as trivial and I am still trying to figure it out

the 2nd one can be proven over the first, and maybe in a more general context — the witness seems sth like `concat : list (list t) -> list t`

?

maybe easier to write as

```
Definition on_one A (R:relation A) (l l' : list A) :=
exists l0 l1 x y, l = l0 ++ x :: l1 /\ l' = l0 ++ y :: l1 /\ R x y.
Definition one_by_one A R l l' := reflexive_transitive_closure (on_one A R) l l'.
```

then you want to prove `size b = size b' -> b [-->*] b' -> one_by_one _ (-->*) b b'`

and it should also be possible to prove `on_one A (reflexive_transitive_closure A R) l l' -> one_by_one A R l l'`

(reflexive_transitive_closure is called Relation_Operators.clos_refl_trans in the stdlib)

Paolo Giarrusso said:

the 2nd one can be proven over the first, and maybe in a more general context — the witness seems sth like

`concat : list (list t) -> list t`

?

I am not sure I understand, I assume mean using the first one ?

This is what I am trying.

```
Require Import List Relation_Operators Relation_Definitions RelationClasses.
Import ListNotations.
Definition on_one {A} (R:relation A) (l l' : list A) :=
exists l0 l1 x y, l = l0 ++ x :: l1 /\ l' = l0 ++ y :: l1 /\ R x y.
Definition one_by_one {A} R l l' := clos_refl_trans _ (@on_one A R) l l'.
#[export] Instance one_by_one_refl A R : Reflexive (@one_by_one A R).
Proof.
red; apply rt_refl.
Qed.
#[export] Instance one_by_one_trans A R : Transitive (@one_by_one A R).
Proof.
Search clos_refl_trans.
red; apply rt_trans.
Qed.
Definition listify {A B} (R:A -> B -> Prop) l l' := forall p, In p (combine l l') -> R (fst p) (snd p).
Lemma Forall2_listify {A B} R l l' : Forall2 R l l' -> @listify A B R l l'.
Proof.
unfold listify.
induction 1;simpl.
- tauto.
- intros p [[]|?].
+ simpl;assumption.
+ auto.
Qed.
Lemma listify_Forall2 {A B} R l l' : @listify A B R l l' -> length l = length l' -> Forall2 R l l'.
Proof.
revert l';
induction l as [|a l IHl];intros [|b l'];
simpl;try discriminate;intros H Hlen;constructor.
- apply (H (a,b)).
simpl;auto.
- apply IHl.
+ intros p Hp. apply H;simpl;auto.
+ congruence.
Qed.
Lemma on_one_singleton A (R:relation A) x y : R x y -> @on_one A R [x] [y].
Proof.
intros;exists [], [], x, y;auto.
Qed.
Lemma on_one_cons A R l l' x : @on_one A R l l' -> on_one R (x :: l) (x :: l').
Proof.
intros [l0 [l1 [v [v' [Hl [Hl' H]]]]]].
exists (x :: l0), l1, v, v'.
simpl.
intuition;
f_equal;auto.
Qed.
Lemma on_one_app A R l0 l1 l l' : @on_one A R l l' -> on_one R (l0 ++ l ++ l1) (l0 ++ l' ++ l1).
Proof.
intros [lstart [lend [v [v' [Hl [Hl' H]]]]]].
subst;simpl.
exists (l0 ++ lstart), (lend ++ l1), v, v'.
rewrite <-!app_assoc;simpl.
auto.
Qed.
Lemma one_by_one_cons A R l l' x : @one_by_one A R l l' -> one_by_one R (x :: l) (x :: l').
Proof.
induction 1.
- apply rt_step,on_one_cons;assumption.
- reflexivity.
- etransitivity;eassumption.
Qed.
Lemma one_by_one_app A R l0 l1 l l' : @one_by_one A R l l' -> one_by_one R (l0 ++ l ++ l1) (l0 ++ l' ++ l1).
Proof.
induction 1.
- apply rt_step,on_one_app;assumption.
- reflexivity.
- etransitivity;eassumption.
Qed.
Lemma Forall2_one_by_one {A} R (Hr : Reflexive R) l l' : Forall2 R l l' -> @one_by_one A R l l'.
Proof.
induction 1.
- reflexivity.
- transitivity (y :: l);[|apply one_by_one_cons;assumption].
apply rt_step.
exists [], l, x, y.
simpl.
auto.
Qed.
Lemma commute_closure_one_by_one {A} R l l' : on_one (clos_refl_trans A R) l l' -> one_by_one R l l'.
Proof.
intros [l0 [l1 [v [v' [Hl [Hl' H]]]]]].
subst.
apply (one_by_one_app _ _ l0 l1 [v] [v']).
clear l0 l1.
induction H.
- apply rt_step, on_one_singleton;assumption.
- reflexivity.
- etransitivity;eassumption.
Qed.
Lemma drop_closure_one_by_one {A} R l l' : one_by_one (clos_refl_trans A R) l l' -> one_by_one R l l'.
Proof.
induction 1.
- apply commute_closure_one_by_one;assumption.
- reflexivity.
- etransitivity;eassumption.
Qed.
Lemma listify_one_by_one {A} R l l'
: length l = length l' -> listify (clos_refl_trans A R) l l' -> one_by_one R l l'.
Proof.
intros Hlen H.
apply drop_closure_one_by_one,Forall2_one_by_one.
{ red;apply rt_refl. }
apply listify_Forall2;assumption.
Qed.
```

you really have my gratitude, I will try to no look at it until I am really exhausted all my ideas.

also you make it sound easy, I think I know my mistake, not doing that:

```
Definition on_one A (R:relation A) (l l' : list A) :=
exists l0 l1 x y, l = l0 ++ x :: l1 /\ l' = l0 ++ y :: l1 /\ R x y.
Definition one_by_one A R l l' := reflexive_transitive_closure (on_one A R) l l'.
```

That made proofs cumbersome.

I have hard time getting intuition for `one_by_one`

it is R + relexivity and transitivity but I cannot have more high level inutition, for instance I cannot see how does that relate it to `Forall2`

Let's use as example `R x y := y = S x`

, so `clos_refl_trans R x y`

is `x <= y`

we have `listify (clos_refl_trans R) [1; 3; 2] [2; 3; 5]`

which basically means `1 <= 2`

`3 <= 3`

and `2 <= 5`

from this we get `one_by_one R [1; 3; 2] [2; 3; 5]`

which gives a sequence `on_one R [1; 3; 2] [2; 3; 2]`

, `on_one R [2; 3; 2] [2; 3; 3]`

, `on_one R [2; 3; 3] [2; 3; 4]`

, `on_one R [2; 3; 4] [2; 3; 5]`

you can also visualize like this:

diag.png

in listify / Forall2 everything happens at once

in one_by_one at each step the list is changed by exactly one step of R at exactly one element (in the blue square)

Last updated: Nov 29 2023 at 20:01 UTC