walker (Jul 03 2023 at 15:36): walker (Jul 03 2023 at 15:36):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.
Gaëtan Gilbert (Jul 03 2023 at 15:45):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
walker (Jul 04 2023 at 09:08):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?
walker (Jul 04 2023 at 09:09):Also how did you come up with this idea ? is this a known pattern ?
Gaëtan Gilbert (Jul 04 2023 at 09:31):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
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 recbs' nonempty then last b bs' = last b (b1 :: bs') = b' and you have a transitivity stepyou 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 [-->*]
walker (Jul 04 2023 at 11:05):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
walker (Jul 04 2023 at 11:09):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
Gaëtan Gilbert (Jul 04 2023 at 11:19):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
walker (Jul 04 2023 at 11:21):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.
Gaëtan Gilbert (Jul 04 2023 at 11:36):I looked at the constructors you gave for --> and tried to figure out how [-->*] could be expressed in a way compatible with them
walker (Jul 04 2023 at 12:46):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 ?
Paolo Giarrusso (Jul 04 2023 at 12:47):unrelated
Paolo Giarrusso (Jul 04 2023 at 12:50):or, I'd say mostly unrelated but... step-indexing lets you use _fuel_ to define propositions
Paolo Giarrusso (Jul 04 2023 at 12:50):and when reasoning about programs, if e -> e', you typically have one less fuel unit when talking about e'.
Paolo Giarrusso (Jul 04 2023 at 12:52):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
walker (Jul 04 2023 at 12:53):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.
Paolo Giarrusso (Jul 04 2023 at 12:54):one can't be an expert in everything :-)
walker (Jul 04 2023 at 12:54):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
Paolo Giarrusso (Jul 04 2023 at 13:00):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?
Gaëtan Gilbert (Jul 04 2023 at 13:02):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'
Gaëtan Gilbert (Jul 04 2023 at 13:03):(reflexive_transitive_closure is called Relation_Operators.clos_refl_trans in the stdlib)
walker (Jul 04 2023 at 13:07):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.
Gaëtan Gilbert (Jul 04 2023 at 13:49):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.
walker (Jul 04 2023 at 14:37):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.
walker (Jul 05 2023 at 07:43):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
Gaëtan Gilbert (Jul 05 2023 at 08:38):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