walker (Feb 12 2024 at 10:19): walker (Feb 12 2024 at 10:19):I have this list relation:
Inductive ListRel A (R: A -> A -> Prop) (f: A -> nat -> A -> A): seq A -> seq A -> Prop :=
| ListRel_empty: ListRel R f [::] [::]
| ListRel_cons t1 T1 ts Ts:
R t1 T1 ->
ListRel R f ts (imap (f t1) Ts) ->
ListRel R f (t1::ts) (T1::Ts).
Where imap is just indexed map function: (nat -> A -> B) -> seq A -> seq B
It usage arise when having to type list of parameters and indices in formalizing inductive families. Ideally I use to say list of params p has type of list of param types P. The need for imap is because P[1] requires var 0 to be replaced with p[0]. But P[2] will require var 1 to be replaced with p[0]...etc.
And I can tell that it works (using lots of examples an tests), but from metatheory perspective. I cannot prove anything about it aside from this lemma:
ListRel R1 s Γ1 Γ2 ->
(forall a b, R1 a b -> R2 a b) ->
ListRel R2 s Γ1 Γ2.
The most important property I need to prove about this relation is how it interacts with map
Like ??? -> Listrel R s (map f Γ1) Γ2 or ??? -> Listrel R s (map f Γ1) (map f Γ2). From less abstract level, this f is usually a substitution. and generally Γ2 is closed telescope. The poblem is I couldn't fill the ??? let alone prove it.
The problem is everytime I try to touch Γ1 Γ2 I get an anoying imap f ... is the goal but it is never in the induction hypothesis.
Mario Carneiro (Feb 12 2024 at 10:47):Here's a lean proof, I'll work out a coq version later if someone doesn't beat me to it but it should be basically the same. This is an instance of some general parametricity argument:
def imap {A B} (f : Nat → A → B) : List A → List B
| [] => []
| a::l => f 0 a :: imap (fun n => f (n + 1)) l
theorem imap_map {A₁ A₂}
(g : A₁ → A₂) (f₁ : Nat -> A₁ -> A₁) (f₂ : Nat -> A₂ -> A₂) (l : List A₁)
(H : ∀ n b, g (f₁ n b) = f₂ n (g b)) :
List.map g (imap f₁ l) = imap f₂ (List.map g l) := by
induction l generalizing f₁ f₂ with simp [*, imap, List.map]
| cons a l ih => apply ih; intros; apply H
inductive ListRel {A B} (R: A -> B -> Prop) (f: A -> Nat -> B -> B): List A -> List B -> Prop :=
| empty: ListRel R f [] []
| cons t1 T1 ts Ts:
R t1 T1 ->
ListRel R f ts (imap (f t1) Ts) ->
ListRel R f (t1::ts) (T1::Ts)
theorem ListRel.map
{A₁ B₁} (R₁: A₁ -> B₁ -> Prop) (f₁: A₁ -> Nat -> B₁ -> B₁)
{A₂ B₂} (R₂: A₂ -> B₂ -> Prop) (f₂: A₂ -> Nat -> B₂ -> B₂)
(ga : A₁ → A₂) (gb : B₁ → B₂)
(H1 : ∀ a n b, gb (f₁ a n b) = f₂ (ga a) n (gb b))
(H2 : ∀ a b, R₁ a b → R₂ (ga a) (gb b))
{l₁ l₂} (H : ListRel R₁ f₁ l₁ l₂) :
ListRel R₂ f₂ (l₁.map ga) (l₂.map gb) := by
induction H with
| empty => exact .empty
| cons t1 T1 ts Ts h1 _ ih =>
exact .cons _ _ _ _ (H2 _ _ h1) (imap_map _ _ _ _ (H1 _) ▸ ih)
gb (f₁ a n b) = f₂ (ga a) n (gb b) I cannot say I am expert, but hoping for this to hold feels like a long shot, but I can try
Mario Carneiro (Feb 12 2024 at 10:53):well you have several degrees of freedom there, you get to pick all four functions and just have to make sure they commute in that way
Mario Carneiro (Feb 12 2024 at 10:54):ga or gb may be an identity function if you don't want to map that side
Mario Carneiro (Feb 12 2024 at 10:55):It's also possible to restrict the identity to only hold on values "contained in" the original lists, if that helps
walker (Feb 12 2024 at 11:06):I get it, I will try and hope everything works, :fingers_crossed: I am so close to finally having fully formalized indexed families
walker (Feb 12 2024 at 14:01):This is almost correct, it is just to general, in my case, H1 and H2 never holds univerally, but they hold for a b when whey are drawn from l1 and l2. except for b is not exactly drawn from l2 and it kind of depends on parts of l1. So I have to figure that part out
walker (Feb 12 2024 at 16:33):So I am stuck somwhere ... let me show where:
I need strong relation that describes: map g (imap_rec f1 l n) = imap_rec f2 (map g l) n.
I already had a different definition of imap (to make induction easier for other cases):
Section IMAP.
Variable A B: Type.
Variable f: nat -> A -> B.
Fixpoint imap_rec (l : seq A) (n : nat) : seq B :=
match l with
| [::] => [::]
| hd :: tl => f n hd :: imap_rec tl n.+1
end.
Definition imap (l : seq A) := imap_rec l 0.
End IMAP.
Then I have:
Lemma imap_rec_map_map_imap_rec A B f1 f2 (g: A -> B) l n:
(forall b m, PIn b l -> g (f1 m b) = f2 m (g b)) ->
map g (imap_rec f1 l n) = imap_rec f2 (map g l) n.
Which I can prove easily ... but that is not good enough I need a restriction on n something like if the mth index of the list l is b
Lemma imap_rec_map_map_imap_rec A B f1 f2 (g: A -> B) l n:
(forall b l1 l2, l = l1 ++ b ++ l2 -> g (f1 (n+size l1) b) = f2 (n + size l1) (g b)) ->
map g (imap_rec f1 l n) = imap_rec f2 (map g l) n.
but this doesn't work for proof by induction on l and I kinda feel stuck
Mario Carneiro (Feb 13 2024 at 00:57):That theorem looks like it would be a bit difficult to use, but you can still prove it by induction:
variable {A B: Type}
variable (f: Nat -> A -> B)
def imap_rec (l : List A) (n : Nat) : List B :=
match l with
| [] => []
| hd :: tl => f n hd :: imap_rec tl (n+1)
def imap (l : List A) := imap_rec f l 0
theorem imap_rec_map_map_imap_rec {A B} (f1 f2) (g: A -> B) (l : List A) (n)
(H : ∀ b l1 l2, l = l1 ++ [b] ++ l2 -> g (f1 (n+l1.length) b) = f2 (n + l1.length) (g b)) :
List.map g (imap_rec f1 l n) = imap_rec f2 (List.map g l) n := by
induction l generalizing n with
| nil => rfl
| cons a l IH =>
simp [imap_rec, List.map]; constructor
· exact H a [] l rfl
· refine IH (n+1) fun b l1 l2 eq => ?_
rw [Nat.add_right_comm]
exact H b (a::l1) l2 (eq ▸ rfl)
Or maybe you are saying that you are having difficulty using this lemma in the proof of ListRel_map?
Mario Carneiro (Feb 13 2024 at 02:19):Here's a general approach to adding constraints on the identities, using arbitrary propositions P and Q as a kind of inductive hypothesis:
variable {A B: Type}
variable (f: Nat -> A -> B)
def imap_rec (l : List A) (n : Nat) : List B :=
match l with
| [] => []
| hd :: tl => f n hd :: imap_rec tl (n+1)
def imap (l : List A) := imap_rec f l 0
def iall (P : A → Nat → Prop) : List A → Nat → Prop
| [], _ => True
| a :: l, n => P a n ∧ iall P l (n + 1)
theorem imap_rec_map_map_imap_rec {A B} (f1 f2) (g: A -> B)
(P : A → Nat → Prop)
(H1 : ∀ b n, P b n -> g (f1 n b) = f2 n (g b))
{l n} (H3 : iall P l n) : List.map g (imap_rec f1 l n) = imap_rec f2 (List.map g l) n := by
induction l generalizing n with
| nil => rfl
| cons a l IH =>
have ⟨hp, hq⟩ := H3
simp [imap_rec, List.map]; constructor
· exact H1 _ _ hp
· exact IH hq
theorem imap_map_map_imap {A B} (f1 f2) (g: A -> B)
(P : A → Nat → Prop)
(H1 : ∀ b n, P b n -> g (f1 n b) = f2 n (g b))
{l} (H3 : iall P l 0) : List.map g (imap f1 l) = imap f2 (List.map g l) :=
imap_rec_map_map_imap_rec _ _ _ _ H1 H3
inductive ListRel {A B} (R: A -> B -> Prop) (f: A -> Nat -> B -> B): List A -> List B -> Prop :=
| empty: ListRel R f [] []
| cons t1 T1 ts Ts:
R t1 T1 ->
ListRel R f ts (imap (f t1) Ts) ->
ListRel R f (t1::ts) (T1::Ts)
theorem ListRel.map
{A1 B1} (R1: A1 -> B1 -> Prop) (f1: A1 -> Nat -> B1 -> B1)
{A2 B2} (R2: A2 -> B2 -> Prop) (f2: A2 -> Nat -> B2 -> B2)
(P : B1 → Nat → Prop) (Q : List B1 → Prop)
(ga : A1 → A2) (gb : B1 → B2)
{L1 L2}
(H1 : ∀ a b n, a ∈ L1 → P b n → gb (f1 a n b) = f2 (ga a) n (gb b))
(H2 : ∀ a b, R1 a b → R2 (ga a) (gb b))
(H3 : Q L2)
(H4 : ∀ t1 t2 l2, R1 t1 t2 → t1 ∈ L1 → Q (t2::l2) → iall P l2 0 ∧ Q (imap (f1 t1) l2))
(H : ListRel R1 f1 L1 L2) :
ListRel R2 f2 (L1.map ga) (L2.map gb) := by
induction H with
| empty => exact .empty
| cons t1 T1 ts Ts h1 _ ih =>
have ⟨HP, H4'⟩ := H4 _ _ _ h1 (.head _) H3
refine .cons _ _ _ _ (H2 _ _ h1) (imap_map_map_imap _ _ _ P ?_ HP ▸ ih ?_ H4' ?_)
· intro b n h
exact H1 t1 b n (.head _) h
· intro a b n h1 h2
exact H1 a b n (.tail _ h1) h2
· intro t1 t2 l2 h1 h2
exact H4 _ _ _ h1 (.tail _ h2)
I don't really know enough about your setting to know whether hypothesis H4 can be simplified to something non-recursive or without using imap in the statement. The difficulty is that at each stage of the recursion f is applied again to the tail of the list, so it's not enough to know that the elements of L2 are "good", they have to remain good after applying f, or the n'th element needs to be good after applying f exactly n times, or other variations like that.
By choosing P and Q appropriately you can express these things, for example to get the statement involving forall b l1 l2, l = l1 ++ b ++ l2 -> that you wrote you can take P to be fun a n => ∃ l1 l2, l = l1 ++ [a] ++ l2 ∧ n = l1.length.
walker (Feb 13 2024 at 08:25):apparently imap_rec_map_map_imap_rec was not as hard as I thought, i was just exhausted being end of day. What I meant to say is that the main theorem ListRel.map is too weak but I am in the process of trying to fix it again.
for both H1 H2, terms a, and b are abitrary. but in my case the the two preconditions H1 H2 only holds for term selected from L1 and L2, and it has to be precisely the corresponding elements of the list, becuase in my case they are part of well scoped list of terms and types, and the resulting H1 and H2 only holds when the scope fulfil certain conditions.
walker (Feb 13 2024 at 08:27):that is why I needed imap_rec_map_map_imap_recand imap_map_map_imapto talk about the exact location of that element be where g (f1 m b) = f2 m (g b) and just saying that b was memeber of the list was not enough
Mario Carneiro (Feb 13 2024 at 09:51):In the last code block I posted, a and b are not arbitrary, they must satisfy predicate P a b and you can put whatever well scoped something something in there. I think it would be best not to refer to the original list L1, as this significantly complicates things; instead state whatever property you need about the list and prove that L1 has that property
walker (Feb 13 2024 at 09:54):wow some how I missed that, I was hunting for in relation or similar things! I will study this thing carefully now, thanks for pointing this again
walker (Feb 13 2024 at 09:55):thanks a lot!
walker (Feb 13 2024 at 10:26):That is a neat generalization you got! I like it it took me a moment to notice what is going on there
walker (Feb 13 2024 at 10:26):The only problem is that P is never inferable which is not entirely bad.
walker (Feb 13 2024 at 13:19):I still do nothave full intution for what Q is generally speaking
walker (Feb 15 2024 at 14:40):So, Back to where I was :\ I think I found the correct generalization, ListRel depended alot on many many properties of debruijn substitution. The correct generalization It is just a seq_forallpair instead of that ugly looking ListRel. Where seq_forallpair holds relation for all elements of two lists.
Now I have all lots of nice properties, But the wierd imap logic had to be placed somewhere, and for that I created custom funtion:
Fixpoint subst_params_indices (pi: seq Term) (PI: seq Term): (seq Term) :=
match pi, PI with
| nil, _ => PI
| _, nil => nil
| p::pi', P::PI' => P:: (subst_params_indices pi' (imap (fun i => subst (upn i (p .: ids))) PI'))
end.
Intuitively, this function accepts two list of terms pi which is is list of parameters and PI which is comes from a telescope, usually such that, and what this function does is subttitute each parameter into its right location in the telescope. But this imap is ugly and makes proofs about this function much much complex.
For instance I always have lemmas like:
Lemma map_cat_ext A B (f: A -> B) (p: seq A) (p1 p2: seq B):
[seq f i | i <- p] = p1 ++ p2 <->
exists p1' p2',
[seq f i | i <- p1'] = p1 /\
[seq f i | i <- p2'] = p2 /\
p = p1' ++ p2'.
But it is extremely tricky to do the same (among many other things) for this subst_params_indices.
So is there away to decompose subst_params_indices such that it is less pain to work with ?
walker (Feb 15 2024 at 14:42):Also it will be great if the right moderator, can help me move this to metacoq, not because this is metacoq related, but the I expect that metacoq developers must have faced similar problem at some point in time @Cyril Cohen ?
Meven Lennon-Bertrand (Feb 19 2024 at 16:30):I believe on the MetaCoq side (and in pen-and-paper accounts too), when you want to type a telescope/parallel substitution, you typically type it in "snoc" order. That is, the empty telescope is well-typed at the empty type, and a telescope (σ,t) is of type Γ,T if 1) σ is of type Γ and t is of type T[σ]. This should make things easier, because the "recursive" part does not need any substitution…
walker (Feb 19 2024 at 16:41):That is neat trick! don't know what I never thought of that, however, that is not how metacoq does it?
Actually Some time later, I had similar question in metacoq, and was pointed towards ctx_inst which also does nested recursion using the same approach, the only difference was that metacoq only generalized typing relation, while I generalized substitution and typing relation.
walker (Feb 19 2024 at 16:43):The way I ended up adopting (which did work, and lead me to all stability lemmas) is by having a custom substition function for telescope, which I described here(out of happiness that all proofs work) https://coq.zulipchat.com/#narrow/stream/237658-MetaCoq/topic/Formalizing.20inductive.20families.2E/near/422041073
walker (Feb 19 2024 at 16:43):but actually doing things in reverse order is nicer, and I might rewrite things into that later!
Meven Lennon-Bertrand (Feb 19 2024 at 17:00):Well, there are too many notions of telescope/parallel substitution and their typing in MetaCoq, so ymmv… And many definitions appeared "organically", in retrospect some might be debatable, maybe this is one of them. I guess one good reason not to go with snoc order is that if your telescope is presented as a list of arguments (as is typically the case for inductive type/constructor parameters/indices/arguments), then they will form a list in cons order, and so your approach is more direct.
Last updated: Oct 13 2024 at 01:02 UTC