--- 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/c85d1d5d89d09ec1632320e8448c67fd12/05 13:16
pgiarrusso_gallais_: thanks, will have to study that12/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 terms12/05 13:24
pgiarrusso_fair enough12/05 13:24
pgiarrusso_yeah, well-scoping would give similar problems12/05 13:24
pgiarrusso_I'd have to remove even well-scoping12/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 corrected12/05 13:25
Saizantbh, parallel substitutions usually eliminate the need for swapping things, but i can image not everywhere12/05 13:30
pgiarrusso_Saizan: my problem arose by looking at an eta-reduction rule: (\x . ((weaken x t) x) =βη t12/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)) βη-≡ t12/05 13:47
pgiarrusso_anyway, thanks for all the advise12/05 13:51
pgiarrusso_*advice12/05 13:51
Saizanpgiarrusso_: 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 derivations12/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-L19212/05 14:30
Saizanoh, 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 lemma12/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 substitution12/05 14:34
pgiarrusso_that *might* be entirely my fault12/05 14:34
Saizanmh, I wouldn't even use the Shub thing much, but anyway i think it wouldn't be that bad12/05 14:39
Saizanyou 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 split12/05 14:40
* Saizan wants autosubst in Agda12/05 14:42
gallais_pgiarrusso_: bruteforce: https://gist.github.com/gallais/c85d1d5d89d09ec1632320e8448c67fd12/05 14:43
pgiarrusso_gallais_: oh dear, how ugly was that?12/05 14:45
gallais_not too bad12/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 now12/05 14:56
pgiarrusso_so I shouldn't bug you too much12/05 14:56
pgiarrusso_anyway, thanks for showing what is in fact possible :-)12/05 14:56
Saizanpgiarrusso_: http://www2.tcs.ifi.lmu.de/~abel/guarded-normalization/Substitution.html#1 <- something like this, except for the SubCong junk12/05 15:01
pgiarrusso_Saizan: thanks12/05 15:02
pgiarrusso_Saizan: what's +1? Your link uses other stuff. I've used suc, but that won't work under abstractions—instead of suc, I need something that leaves the first variable alone—which I have defined12/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 case12/05 15:52
pgiarrusso_I can massage the goal so that I get induction on a new `r`, but I can't get +112/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 guess12/05 16:12
Saizanpgiarrusso_: but where would you use this?12/05 16:13
Saizanit shouldn't be needed for eta, t is in Gamma, the body of the lambda is in "Gamma , T", so you just need suc12/05 16:14
pgiarrusso_Saizan: uh sorry, that's under lambda, because I was also looking at weakenings for terms12/05 16:15
pgiarrusso_sorry for the confusion12/05 16:16
Saizanwhat 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 // t12/05 16:17
pgiarrusso_where t is a term12/05 16:17
pgiarrusso_while you where talking about equality derivations, as I mentioned originally12/05 16:17
pgiarrusso_Anyway, I'll stop bothering you12/05 16:18
pgiarrusso_because I'd need to do much more homework first12/05 16:18
Saizanmy "=" was propositional equality, because i thought that would be the goal needed to weaken the eta constructor, but icbw12/05 16:18
pgiarrusso_oh right12/05 16:19
pgiarrusso_propositional equality would probably work... but the same problem applies12/05 16:22
pgiarrusso_I get goal wkθ σ₁ (wkθ σ (ren r)) // wkθ σ₁ (ren (λ {.τ} → vs)) // t ≡ wkθ σ₁ (ren (λ {.τ} → vs)) // wkθ σ₁ (ren r) // t12/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 go12/05 16:26
Saizanyou 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 equality12/05 16:41
lambdabotConsider it noted.12/05 16:41

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