Match on _IsRelatedTo_ later for the PartialSetoid Reasoning

[Ailrun]

Main Motivation of This PR

The current version does not work in the following case, for example:

begin A ≈⟨ some-partial-equiv ⟩
      B ≡⟨ some-complex-eq ⟩
      C ∎

when some-complex-eq is not definitionally equal to refl. Because of that, step of the noncomputing syntax will not be evaluated, and in turn, ∼-go does not produce any multiStep constructor. This blocks the decision procedure IsMultiStep?.

One can make this work using subst, but more complex reasoning becomes very nasty with that.

This PR makes the above example work.

Related Issue

One related, remaining issue is that the reversed case still does not work:

begin A' ≡⟨ some-complex-eq' ⟩
      B' ≈⟨ some-partial-equiv' ⟩
      C' ∎

As some-complex-eq is not definitionally equal to refl, step of the noncomputing syntax will not be evaluated. Thus, like before, IsMultiStep? cannot decide whether this reasoning contains multiple steps or not.

[jamesmckinna]

I would personally find an example helpful here to illustrate the discussion.

Specifically, to understand in your hypothetical first situation if, and then why, the following reasoning would not work instead:

begin A ≈⟨ some-partial-equiv ⟩
      B ≈⟨ reflexivity (some-complex-eq) ⟩
      C ∎

It may be that some (other) plumbing may be required, such as observing that reflexivity holds in PERs at any B such that p : A ≈ B for some p, A, and whether or not that might also work in the second situation?

Certainly, the library has no examples of reasoning in PERs that I'm aware of, so it probably hasn't been stress tested enough for the situations you sketch.

[Ailrun]

@jamesmckinna some-complex-eq is a proof of propositional equality, not an equivalence I am using, so it is impossible to use ≈⟨⟩ as far as I know. Maybe I should have clarified that I have a PER different from the propositional equality and which proof of my example uses which one amongst them.

Here is the list:

• some-partial-equiv : A ≈ B where _≈_ is a PER (different from the propositional equality)
• some-complex-eq : B ≡ C
• some-complex-eq' : A' ≡ B'
• some-partial-equiv' : B' ≈ C'

[jamesmckinna]

( I updated my posting to try to make clearer my intentions)

[Ailrun]

@jamesmckinna The problem there is, _≈_ is a PER, so B ≡ C does not give B ≈ C. That entire thing works only because there is A ≈ B already where we can apply a substitution on (namely, substitute C for B in A ≈ B using B ≡ C).

[Ailrun]

@jamesmckinna One can prove something like

begin A ≈⟨ some-partial-equiv ⟩
      B ≈⟨ right-reflexivity some-partial-equiv some-complex-eq ⟩
      C ∎

with right-reflexivity that derive B ≈ C out of A ≈ B and B ≡ C, but then the problem is when we have multiple steps of equalities:

begin A ≈⟨ some-partial-equiv ⟩
      B ≡⟨ eq1 ⟩
      C ≡⟨ eq2 ⟩
      D ≡⟨ eq3 ⟩
      E ≡⟨ eq4 ⟩
      F ≡⟨ eq5 ⟩
      G ∎

Now, to change eq5 into F ≈ G, we need to derive X ≈ F for some X (or the symmetric one), but if no other information is given, the only obvious such proof is applying subst on some-partial-equiv to change B with F, which is basically the whole proof.

[jamesmckinna]

@Ailrun thanks very much for the clarification, and sorry that my efforts last night weren't quite enough to make myself clear.

What I had in mind was the following plumbing, for PER _≈_:

  trans-reflˡ : ∀ {x y z} → x ≡ y → y ≈ z → x ≈ z
  trans-reflˡ ≡.refl p = p

  trans-reflʳ : ∀ {x y z} → x ≈ y → y ≡ z → x ≈ z -- by analogy with `Relation.Binary.PropositionalEquality.trans-reflʳ`
  trans-reflʳ p ≡.refl = p

  p-reflˡ : ∀ {x y} → x ≈ y → x ≈ x -- 'partial reflexivity on the left'
  p-reflˡ p = trans p (sym p)

  p-reflʳ : ∀ {x y} → x ≈ y → y ≈ y
  p-reflʳ p = trans (sym p) p

  p-reflexiveˡ : ∀ {x y z} → x ≈ y → x ≡ z → x ≈ z
  p-reflexiveˡ p ≡.refl = p-reflˡ p

  p-reflexiveʳ : ∀ {x y z} → x ≈ y → y ≡ z → y ≈ z
  p-reflexiveʳ p ≡.refl = p-reflʳ p

and then to replace your

begin A ≈⟨ p ⟩
      B ≡⟨ q ⟩
      C ∎

by

begin A ≈⟨ p ⟩
      B ≈⟨ p-reflexiveʳ p q ⟩
      C ∎

and the second example similarly (?).

But your question does indeed draw attention to problems with the current setup! And that my suggestions are certainly not per se part of the current Reasoning setup. The chains of reasoning argument is also quite compelling, even if B ≡ F would be provable by a sub-chain of _≡_-reasoning.

I've encountered something similar in the Pointwise theory of List, but 'solved' it by appeals to such reflexivity wrappers.

Does the solution in the current PR completely solve the problem, however? I'd be happier if we had did have such...

[Ailrun]

To be honest, I don't think this PR's solution is really a complete solution. I intended to give a solution with a minimal impact in the sense that it does not "reduce" the reduction behavior. If we want a more complete solution, my guess is changing _IsRelated_ to track equalities as well (I believe strict order case has such tracking). That change would solve both of the "problematic" cases I mentioned in the original post.

[jamesmckinna]

Thanks! It would be good for the implementor(s) of the original reasoning setup to comment here I think... @MatthewDaggitt ?

[MatthewDaggitt]

To be honest, I don't think this PR's solution is really a complete solution. I intended to give a solution with a minimal impact in the sense that it does not "reduce" the reduction behavior. If we want a more complete solution, my guess is changing IsRelated to track equalities as well (I believe strict order case has such tracking). That change would solve both of the "problematic" cases I mentioned in the original post.

I agree with your analysis. Changing _IsRelated_ to track equalities seems like the more principled solution. Do you think you would have the time to have a crack at it @Ailrun?

[Ailrun]

@MatthewDaggitt Unfortunately not within a month. After a month I might have some more time.