Problem is here...

[Ailrun]

No description provided.

[Ailrun]

With the current rel_exp_under_ctx, it is not possible to give the correct R here.
However, with

Definition rel_exp_under_ctx Γ M M' A :=
  exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }}) i
     (elem_rel : forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}), relation domain),
  forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
     rel_typ i A p A p' (elem_rel _ _ equiv_p_p') /\ rel_exp (elem_rel _ _ equiv_p_p') M p M' p'.

now the problem is in rel_exp_sub_cong... its last eexists requires equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }} to destruct some Props.

[HuStmpHrrr]

let's discuss next week. there might just be an easy way out.

[Ailrun]

@HuStmpHrrr with

instantiate (1 := fun c c' (equiv_c_c' : head_rel p p' equiv_p_p' c c') b b' =>
  forall a a' R,
    {{ ⟦ B ⟧ p ↦ c ↘ a }} ->
    {{ ⟦ B' ⟧ p' ↦ c' ↘ a' }} ->
    per_univ_elem i a a' R ->
    R b b').

Now the problem is that we need to show

per_univ_elem i m m'0
    (fun b b' : domain =>
     forall (a0 a'0 : domain) (R : relation domain),
     {{ ⟦ B ⟧ p ↦ c ↘ a0 }} -> {{ ⟦ B' ⟧ p' ↦ c' ↘ a'0 }} -> per_univ_elem i a0 a'0 R -> R b b')

under

H : per_univ_elem i m m'0 R'

Here the main problem is that even when we know R that satisfies per_univ_elem i a0 a'0 R, this R is not equal to per_univ_elem i a0 a'0 R -> R b b' (or any similar variant).

[Ailrun]

In other words, this approach looks like requiring propositional extensionality to work.

[Ailrun]

Basically it goes back to the dependence issue of ?out_rel. It can be solved by either

1. your way with propositional extensionality
2. a more "naive" way with dep. choice (or indef. descr.)

But would there be a better way (that requires weaker/no axioms)?

[HuStmpHrrr]

I think the change to the PER model is more substantial. It should use <-> to relate the returning relation in all cases. let's merge the other PR first, and then try to see how this fix complicates the proofs.

[Ailrun]

Yeah, that approach requires some "congruence-like" lemmas like the one you suggested, and that makes all other cases also contain R <-> per_nat or so.

[Ailrun]

It seems like we need to understand the structure of per_elems better first. By that I mean equivalence relation we want to use between those (previously: equality, suggestion: biconditional), or in general, what kind of "morphisms" (and isomorphisms) we have between those.

Then per_univ_elem i - a a' should respect that (iso-)morphisms.

[Ailrun]

Actually, the new equivalence is in fact not just biconditional, but a biconditional under some universal quantification and applications. Under this, do we need fun. ext.? I mean, the arguments we need to add here would be something like forall a b, R a b <-> per_nat a b or so, which already has all arguments. Hm... let's see after changing the PER type.

[HuStmpHrrr]

It seems like we need to understand the structure of per_elems better first. By that I mean equivalence relation we want to use between those (previously: equality, suggestion: biconditional), or in general, what kind of "morphisms" (and isomorphisms) we have between those.

Then per_univ_elem i - a a' should respect that (iso-)morphisms.

same thought.

Actually, the new equivalence is in fact not just biconditional, but a biconditional under some universal quantification and applications. Under this, do we need fun. ext.? I mean, the arguments we need to add here would be something like forall a b, R a b <-> per_nat a b or so, which already has all arguments. Hm... let's see after changing the PER type.

yeah, I meant an equivalence between relations. There should be something already defined in the standard library, at least that's what I hope.

[HuStmpHrrr]

I frankly don't understand what is this for. can we avoid this? it's not making the script nice looking. when is mark and unmark useful? most of the time, we should be able to match the exact assumption we want to play with. usually, mark and unmark can be avoided by, for example, failing when detecting repeated hypotheses in the proof context.

[Ailrun]

Yes that would work as well. Marking/unmarking is really an "easy" way to implement something based on traversal, not a "nice" way. Once the PER things are solved, let check what would make tactics better-looking.

[Ailrun]

Just for your information, this change is to allow the use of this tactic within another tactic depending marking.

[Ailrun]

Oh, BTW, there are some cases where marking/unmarking is really meaningful

1. when we apply a tactic to assumptions but that only changes the goal.
2. when we apply an idempotent/self-invertible tactic on hypotheses
3. Although this is not about "applying on all hypotheses" procedures, marking/unmarking can be used to block applications of some (automation-based) tactics to a hypothesis.

[HuStmpHrrr]

yeah, I guess it's an Ltac issue. The usually way I would implement a "saturation" tactic is to do the following:

1. remember the current number of assumptions = n,
2. saturate,
3. remove duplicates,
4. if the current number of assumptions == n, then fail, effectively, this step makes sure some useful saturation is done,
5. repeat step 1-4 until failure.

this way, you don't care about marking or need to use any "difficult" Ltac programming tricks, and it's easier to understand IMO.

[Ailrun]

That approach requires the change of the number of assumptions, but there are cases where we don't have such, like inversion_clear, so that approach is not so general IMO.