--- Day changed Fri May 12 2017 | ||

gallais_ | pgiarrusso_: Not really sure whether that'll deliver the right thing but This is the sort of relation I would try to use: https://gist.github.com/gallais/c85d1d5d89d09ec1632320e8448c67fd | 12/05 13:16 |
---|---|---|

pgiarrusso_ | gallais_: thanks, will have to study that | 12/05 13:17 |

pgiarrusso_ | meanwhile, I realized that http://prosecco.gforge.inria.fr/personal/ckeller/Recherche/hsubst.html does spend work on this problem (though I'm not sure it proves all the lemmas I wanted), though it does take nontrivial work. | 12/05 13:18 |

pgiarrusso_ | gallais_: beyond helping me, do you think such "variable swap" lemmas are often harder with intrinsic types, and do you think the literature has already solved this problem? | 12/05 13:22 |

gallais_ | I have never tried to prove such lemmas so I wouldn't know. | 12/05 13:24 |

gallais_ | I would guess you would have the same problem with "just" well-scoped terms | 12/05 13:24 |

pgiarrusso_ | fair enough | 12/05 13:24 |

pgiarrusso_ | yeah, well-scoping would give similar problems | 12/05 13:24 |

pgiarrusso_ | I'd have to remove even well-scoping | 12/05 13:25 |

pgiarrusso_ | my guess is these lemmas are harder (but maybe it's just me) and this is not really discussed enough by the literature, but I'm very happy to stand corrected | 12/05 13:25 |

Saizan | tbh, parallel substitutions usually eliminate the need for swapping things, but i can image not everywhere | 12/05 13:30 |

pgiarrusso_ | Saizan: my problem arose by looking at an eta-reduction rule: (\x . ((weaken x t) x) =βη t | 12/05 13:44 |

pgiarrusso_ | haven't found a way to express the needed class of parallel substitutions I'd want to a parallel substitution that *never* uses a variable in the target context | 12/05 13:45 |

pgiarrusso_ | (more precisely, I had taken type _βη-≡_ for equivalence, with constructor eta : forall {σ τ} → {t : Tm Γ (σ ⇒ τ)} → Λ (app (wkTm vz t) (var vz)) βη-≡ t | 12/05 13:47 |

pgiarrusso_ | anyway, thanks for all the advise | 12/05 13:51 |

pgiarrusso_ | *advice | 12/05 13:51 |

Saizan | pgiarrusso_: what do you want to prove about that rule? that it's closed under substitutions? | 12/05 14:26 |

pgiarrusso_ | I tried proving I can weaken derivations | 12/05 14:27 |

pgiarrusso_ | and I ended up requiring a lemma about substitution swaps: https://github.com/Blaisorblade/Agda-playground/blob/8b561f74edfc73a44b89526960fd120fc18a3af3/LogicalRelationsEquivChecking/EquivSubst1.agda#L183-L192 | 12/05 14:30 |

Saizan | oh, yeah, your problem might be the definition of "wkTm vz", if that's also done the parallel subsitution way then weakening derivation should just require a small lemma | 12/05 14:30 |

pgiarrusso_ | I proved wkβη-≡ : ∀ {Γ σ τ} (x : Var Γ σ) {t₁ t₂ : Tm (Γ - x) τ} → t₁ βη-≡ t₂ → wkTm x t₁ βη-≡ wkTm x t₂ (note the -), but ended up having to swap two weakening by one variable... | 12/05 14:34 |

pgiarrusso_ | I forget what went wrong when I tried parallel substitution | 12/05 14:34 |

pgiarrusso_ | that *might* be entirely my fault | 12/05 14:34 |

Saizan | mh, I wouldn't even use the Shub thing much, but anyway i think it wouldn't be that bad | 12/05 14:39 |

Saizan | you would have to prove "lift (ren r) // ren (+1) // t = ren (+1) // ren r // t" and modulo composition of substitution and pointwise equality, it's really just a case split | 12/05 14:40 |

* Saizan wants autosubst in Agda | 12/05 14:42 | |

gallais_ | pgiarrusso_: bruteforce: https://gist.github.com/gallais/c85d1d5d89d09ec1632320e8448c67fd | 12/05 14:43 |

pgiarrusso_ | gallais_: oh dear, how ugly was that? | 12/05 14:45 |

gallais_ | not too bad | 12/05 14:45 |

pgiarrusso_ | Saizan: what's the library you have in mind (to lookup lift and so on)? | 12/05 14:47 |

pgiarrusso_ | what I tried looks closer to having `ren (someLift r)` | 12/05 14:54 |

pgiarrusso_ | anyway, this proof is too messed up for now :-| | 12/05 14:55 |

pgiarrusso_ | also, even though I really want to fix this proof, sadly other proofs have higher priority for now | 12/05 14:56 |

pgiarrusso_ | so I shouldn't bug you too much | 12/05 14:56 |

pgiarrusso_ | anyway, thanks for showing what is in fact possible :-) | 12/05 14:56 |

Saizan | pgiarrusso_: http://www2.tcs.ifi.lmu.de/~abel/guarded-normalization/Substitution.html#1 <- something like this, except for the SubCong junk | 12/05 15:01 |

pgiarrusso_ | Saizan: thanks | 12/05 15:02 |

pgiarrusso_ | Saizan: what's +1? Your link uses other stuff. I've used suc, but that won't work under abstractionsinstead of suc, I need something that leaves the first variable alonewhich I have defined | 12/05 15:48 |

pgiarrusso_ | (which I had already defined) | 12/05 15:48 |

pgiarrusso_ | but then `lift (ren r) // ren (+1) // t = ren (+1) // ren r // t` doesn't apply any more to the recursive case | 12/05 15:52 |

pgiarrusso_ | I can massage the goal so that I get induction on a new `r`, but I can't get +1 | 12/05 15:53 |

pgiarrusso_ | or, I can't get `suc` (using the terms from your link) | 12/05 15:53 |

Saizan | "lift suc" would be the thing then, i guess | 12/05 16:12 |

Saizan | pgiarrusso_: but where would you use this? | 12/05 16:13 |

Saizan | it shouldn't be needed for eta, t is in Gamma, the body of the lambda is in "Gamma , T", so you just need suc | 12/05 16:14 |

pgiarrusso_ | Saizan: uh sorry, that's under lambda, because I was also looking at weakenings for terms | 12/05 16:15 |

pgiarrusso_ | sorry for the confusion | 12/05 16:16 |

Saizan | what do you mean? | 12/05 16:16 |

pgiarrusso_ | I was trying to prove fromSaizan : ∀ {Γ Δ σ τ} (r : Ren Γ Δ) → (t : Tm Γ τ) → wkθ σ (ren r) // ren vs // t βη-≡ ren vs // ren r // t | 12/05 16:17 |

pgiarrusso_ | where t is a term | 12/05 16:17 |

pgiarrusso_ | while you where talking about equality derivations, as I mentioned originally | 12/05 16:17 |

pgiarrusso_ | Anyway, I'll stop bothering you | 12/05 16:18 |

pgiarrusso_ | because I'd need to do much more homework first | 12/05 16:18 |

Saizan | my "=" was propositional equality, because i thought that would be the goal needed to weaken the eta constructor, but icbw | 12/05 16:18 |

pgiarrusso_ | oh right | 12/05 16:19 |

pgiarrusso_ | propositional equality would probably work... but the same problem applies | 12/05 16:22 |

pgiarrusso_ | I get goal wkθ σ₁ (wkθ σ (ren r)) // wkθ σ₁ (ren (λ {.τ} → vs)) // t ≡ wkθ σ₁ (ren (λ {.τ} → vs)) // wkθ σ₁ (ren r) // t | 12/05 16:22 |

pgiarrusso_ | The extra weakening wkθ around vs comes from the definition of _//_: | 12/05 16:23 |

pgiarrusso_ | θ // Λ {σ = σ} t = Λ (wkθ σ θ // t) | 12/05 16:23 |

pgiarrusso_ | (which I think does the right thing) | 12/05 16:23 |

pgiarrusso_ | anyway, thanks all, gotta go | 12/05 16:26 |

Saizan | you shouldn't do induction on t.. | 12/05 16:40 |

Saizan | @tell pgiarrusso do not prove this by induction on t, but by some lemmas about substitutions composing and // respecting pointwise equality | 12/05 16:41 |

lambdabot | Consider it noted. | 12/05 16:41 |

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!