[ new ] Tactic.Cong

[dylanede]

Fixes #1136. In doing so, it also adds machinery for applying reflected terms to each other, which could be useful for other tactics in the future.

[dylanede]

I realise now that I've missed out the "Agda Standard Library" blurb at the top of each new file. I'll update the PR soon.

Edit: Done

[MatthewDaggitt]

This is awesome. Thanks so much for putting it together. This is going to be used a lot 😄

I've added a first round of comments (apologies, there's probably likely to be a second round!)

A notation question while we're here. I'm not sure what the origin of using ⌊ and ⌋ in the original holes library was, but I actually find them kind of hard to spot in the big equational reasoning proofs. They're also going to clash with the floor and ceiling functions in Data.Rational (see #1063). Can we replace them with something that stands out better visually?

My tentative suggestion is ⟪ and ⟫ as they would work nicely with the equational reasoning ⟨ and ⟩? But we have lots of options!

[MatthewDaggitt]

It's incredibly neat that we don't have to add it to every version of equational reasoning 🎉

[gallais]

We should probably also have the sym'd one.

[dylanede]

Has syntax been agreed for that yet?

[MatthewDaggitt]

Nope, so maybe leave it out for the moment, and we'll add it in later when we've decided.

[dylanede]

That conflict with functions from Data.Rational is a good point. Maybe I should switch back to ⌞⌟ that agda-holes uses? Personally I'm not overly keen on ⟪_⟫ because in my own code I use that extensively for other purposes, but that probably should not weigh on the decision.

I kind of like the look of 〖〗, but that looks like it is difficult to type in emacs.

[WolframKahl]

I kind of like the look of `〖〗`, but that looks like it is difficult to type in emacs.

I would introduce keyboard shortcuts `\[(` and `\)]` for those.

[nad]

I haven't studied your code, but I have similar code in one of my developments:

• http://www.cse.chalmers.se/~nad/listings/equality/Tactic.By.html
• http://www.cse.chalmers.se/~nad/listings/equality/Tactic.By.Propositional.html
• http://www.cse.chalmers.se/~nad/listings/equality/Tactic.By.Path.html
• http://www.cse.chalmers.se/~nad/listings/equality/Tactic.By.Id.html
• http://www.cse.chalmers.se/~nad/listings/equality/Tactic.By.Parametrised.html
• git clone http://www.cse.chalmers.se/~nad/repos/equality/

I have two tactics, one that tries to infer the context automatically (by), and one that is perhaps more similar to yours (⟨by⟩). The latter one is typically faster, but I often avoid using also this one, because it tends to make type-checking noticeably slower, and it does not handle all code that I would like it to handle. Is your tactic faster? And does it pass all the unit tests in my code (including those that I have commented out)?

[dylanede]

With a revised version of the macro (not yet pushed), proofs like this now work:

qu : (a b c d : ℤ) → a + b + c ≤ d → b + a + c ≤ d
qu a b c d  a+b+c≤d = begin
  ⌊ b + a ⌋ + _ ≡⌊ +-comm b _ ⌋
  a + b + c     ≤⟨ a+b+c≤d ⟩
  d             ∎

Notice that _ can be used in any of the arguments to _≡⌊_⌋_, which is something agda-holes could not do.

This new version depends on a PR I have submitted to Agda itself: agda/agda#4579

Therefore I would like to change this PR to be against experimental instead of master, however experimental seems to be out of date with respect to master currently, so perhaps it should be updated first? @MatthewDaggitt?

@nad: I will have to check your code out at some point.

[dylanede]

I have pushed to this PR the new, reworked version of Tactic.Cong. The build will currently fail since it depends on agda/agda#4579, but you should be able to get a feel of what is now possible by looking at the revamped README module.

[dylanede]

By the way @MatthewDaggitt, I'm marking your review comments as resolved as I go along just as a way of tracking what I have dealt with. Feel free to un-resolve them.

[MatthewDaggitt]

Maybe I should switch back to ⌞⌟ that agda-holes uses?

In my opinion I think those are even less noticeable visually.

Personally I'm not overly keen on ⟪_⟫ because in my own code I use that extensively for other purposes, but that probably should not weigh on the decision.

That's a fine reason, I also use them so I wouldn't be too against avoiding them.

I kind of like the look of 〖〗, but that looks like it is difficult to type in emacs.

I would introduce keyboard shortcuts \[( and \)] for those.

That could definitely work, and I'd be happy with those!

Therefore I would like to change this PR to be against experimental instead of master, however experimental seems to be out of date with respect to master currently, so perhaps it should be updated first? @MatthewDaggitt?

@gallais I've just tried to update experimental and got a massive merge conflict in .travis.yml. I can try and resolve it if you don't have the time, but I'm a little scared of breaking something? Any chance you could take a quick look?

[dylanede]

Slightly off-topic: is there a better font I can use in emacs that is monospace even for symbols like ⦃ and 〖? Or is there a setting I can use in emacs to force fixed width? 〖 for example currently sits at one and a half normal widths, which is a pain. I am using DejaVu Sans Mono.

[nad]

I tried your code. Here are some unit tests:

open import Category.Functor
open import Category.Monad.Indexed
open import Data.Bool
open import Data.List
open import Data.Maybe
import Data.Maybe.Categorical as MC
open import Data.Nat
open import Data.Product
open import Data.Unit
open import Relation.Binary.PropositionalEquality
open import Tactic.Cong.Common
open import Tactic.Cong.PropEq.ForAllTypes 0 _≡_ trans

open ≡-Reasoning
open RawIMonad ⦃ … ⦄

instance

  mm : ∀ {f} → RawIMonad {f = f} {I = ⊤} (λ _ _ → Maybe)
  mm = MC.monad

module _
  (assumption : 48 ≡ 42)
  (lemma      : ∀ n → n + 8 ≡ n + 2)
  (f          : ℕ → ℕ → ℕ → ℕ)
  where

  g : ℕ → ℕ → ℕ → ℕ
  g zero    _ _ = 12
  g (suc _) _ _ = 12

  fst : ∀ {a b} {A : Set a} {B : A → Set b} →
        Σ A B → A
  fst = proj₁

  {-# NOINLINE fst #-}

  test₁ : ⌞ 40 + 2 ⌟ ≡ 42
  test₁ = ⌊⌋ lhs refl

  test₂ : 48 ≡ 42 → ⌞ 42 ⌟ ≡ 48
  test₂ eq = ⌊⌋ lhs (sym eq)

  test₃ : (f : ℕ → ℕ) → f ⌞ 42 ⌟ ≡ f 48
  test₃ f = ⌊⌋ lhs (sym assumption)

  test₄ : (f : ℕ → ℕ) → f ⌞ 48 ⌟ ≡ f 42
  test₄ f = ⌊⌋ lhs assumption

  test₅ : (f : ℕ → ℕ → ℕ) → f ⌞ 42 ⌟ ⌞ 42 ⌟ ≡ f 48 48
  test₅ f = ⌊⌋ lhs (sym assumption)

  test₆ : (f : ℕ → ℕ → ℕ → ℕ) → f ⌞ 48 ⌟ 45 ⌞ 48 ⌟ ≡ f 42 45 42
  test₆ f = ⌊⌋ lhs assumption

  test₇ : f ⌞ 48 ⌟ (f ⌞ 48 ⌟ 45 ⌞ 48 ⌟) ⌞ 48 ⌟ ≡ f 42 (f 42 45 42) 42
  test₇ = ⌊⌋ lhs assumption

  test₈ : ∀ n → g n (g n 45 ⌞ 48 ⌟) ⌞ 48 ⌟ ≡ g n (g n 45 42) 42
  test₈ n = ⌊⌋ lhs assumption

  test₉ : (f : ℕ → ℕ) → f ⌞ 42 ⌟ ≡ f 48
  test₉ f = ⌊⌋ lhs (sym (lemma 40))

  -- test₁₀ : (f : ℕ → ℕ) → f ⌞ 42 ⌟ ≡ f 48
  -- test₁₀ f = ⌊⌋ lhs (λ (_ : ⊤) → assumption)

  test₁₁ : (f : ℕ × ℕ → ℕ × ℕ) → (∀ x → ⌞ _≡_ ⌟ (f x) x) →
           fst ⌞ f (12 , 73) ⌟ ≡ fst {B = λ _ → ℕ} (12 , 73)
  test₁₁ _ hyp = ⌊⌋ lhs (hyp _)

  -- test₁₂ : (h : ℕ → Maybe ℕ) →
  --          ((xs : ℕ) → h xs ≡ just xs) →
  --          (xs : ℕ) → (suc <$> h xs) ≡ (suc <$> return xs)
  -- test₁₂ h hyp xs = begin
  --   suc <$> ⌞ h xs ⌟   ≡⌊ hyp xs ⌋
  --   suc <$> return xs  ∎

  -- test₁₃ : (h : List ⊤ → Maybe (List ⊤)) →
  --          ((xs : List ⊤) → h xs ≡ just xs) →
  --          (x : ⊤) (xs : List ⊤) → _
  -- test₁₃ h hyp x xs = begin
  --   _∷_ <$> return x ⊛ ⌞ h xs ⌟   ≡⌊ hyp xs ⌋
  --   _∷_ <$> return x ⊛ return xs  ∎

  -- test₁₄ : (h : List ℕ → Maybe (List ℕ)) →
  --          ((xs : List ℕ) → h xs ≡ just xs) →
  --          (x : ℕ) (xs : List ℕ) → _
  -- test₁₄ h hyp x xs = begin
  --   _∷_ <$> ⌞ h xs ⌟   ≡⌊ hyp xs ⌋
  --   _∷_ <$> return xs  ∎

  test₁₅ :
    (F : Set → Set → Set)
    (G : Bool → Set → Set) →
    ((A : Set) → F (G false A) A ≡ G false (F A A)) →
    (A : Set) →
    G false (F (G false A) A) ≡
    G false (G false (F A A))
  test₁₅ F G hyp A = begin
    G false ⌞ F (G false A) A ⌟  ≡⌊ hyp _ ⌋
    G false (G false (F A A))    ∎

  test₁₆ : 48 ≡ 42 →
           _≡_ {A = ℕ → ℕ} (λ x → x + ⌞ 42 ⌟) (λ x → x + 48)
  test₁₆ hyp = ⌊⌋ lhs (sym hyp)

  test₁₇ :
    (P : ℕ → Set)
    (f : ∀ {n} → P n → P n)
    (p : P 0) →
    f ⌞ subst P refl p ⌟ ≡ f p
  test₁₇ P _ _ = ⌊⌋ lhs refl

  -- test₁₈ :
  --   (subst′ :
  --      ∀ {a p} {A : Set a} {x y : A}
  --      (P : A → Set p) → x ≡ y → P x → P y) →
  --   (∀ {a p} {A : Set a} {x : A} (P : A → Set p) (p : P x) →
  --    subst′ P refl p ≡ p) →
  --   (P : ℕ → Set)
  --   (f : ∀ {n} → P n → P n)
  --   (p : P 0) →
  --   f ⌞ subst′ P refl p ⌟ ≡ f p
  -- test₁₈ _ subst′-refl _ _ _ = ⌊⌋ lhs (subst′-refl _ _)

I've commented out those test cases that fail. My tactic handles all of the test cases above, except for test₁ and test₁₇. The test cases containing sym also work if sym is removed, and the test cases involving hyp _ or (subst′-refl _ _) work if the underscores are removed from these subexpressions. However, my tactic is rather slow for some of the test cases.

[dylanede]

Thanks for those test cases @nad! I'm working my way through them now.

I've just had a look at the first failure, test₁₀, and I do not understand why that test is meant to pass. The second argument to ⌊⌋ should be of type 42 ≡ 48, but you are providing something of type ⊤ → 48 ≡ 42. This test seems identical in all other respects to test₃. Is there perhaps something lost in translation from your code base?

[dylanede]

Also, which test cases "containing sym" and/or "involving hyp _" are you referring to? All of the ones I can see using those terms are uncommented and work fine. Or did you mean those ones don't work with your tactic?

Oh, I see now that you mean that you mean that your tactic implicitly handles sym-ifying terms and applying metavariables. Personally I am not yet sold on introducing that level of magic.

[dylanede]

test₁₂ (and presumably the others similar to it) is interesting. It exhibits the same problem in this form:

  test₁₂ : (h : ℕ → Maybe ℕ) →
           ((xs : ℕ) → h xs ≡ just xs) →
           (xs : ℕ) → (suc <$> h xs) ≡ (suc <$> return xs)
  test₁₂ h hyp xs = begin
    suc <$> ⌞ h xs ⌟   ≡⟨ ⌊⌋ lhs (hyp xs) ⟩
    suc <$> return xs  ∎

At the point at which ⌊⌋ is called, the lhs, suc <$> ⌞ h xs ⌟, resolves to:

(Category.Applicative.Indexed.RawIApplicative.rawFunctor
 (RawIMonad.rawIApplicative _r_404)
 RawFunctor.<$> suc)
_412

These unsolved metavariables are what is stopping the macro from finding the instance of ⌞⌟ within them. However what is interesting is that if you instead try the following:

  test₁₂ : (h : ℕ → Maybe ℕ) →
           ((xs : ℕ) → h xs ≡ just xs) →
           (xs : ℕ) → (suc <$> h xs) ≡ (suc <$> return xs)
  test₁₂ h hyp xs = begin
    suc <$> ⌞ h xs ⌟   ≡⟨ {!!} ⟩
    suc <$> return xs  ∎

then the lhs of the hole is printed as

(Category.Applicative.Indexed.RawIApplicative.rawFunctor
     (RawIMonad.rawIApplicative
      (MC.monadT Function.Identity.Categorical.monad))
     RawFunctor.<$> suc)
    ⌞ h xs ⌟

So by this point the metavariables have been solved, seemingly with no more information than was available earlier. Indeed, if one now tries to fill the hole with ⌊⌋ lhs (hyp xs), Agda is happy with it, but subsequent reloads of the file fail to typecheck.

[dylanede]

I think solving this might require use of blockOnMeta. It shouldn't change the API though, so I don't think it blocks this PR.

[ajrouvoet]

A notation question while we're here. I'm not sure what the origin of using ⌊ and ⌋ in the original holes library was, but I actually find them kind of hard to spot in the big equational reasoning proofs.

I think that there is something to be said for notation that doesn't steal the show here. They should be unintrusive because you're just trying to read a term whose meaning is not affected by the hole marks. In an on-paper proof you wouldn't mark the whole at all and most and usually you can still easily spot where the rewriting occurs.

[nad]

I think solving this might require use of blockOnMeta.

I'm using blockOnMeta. Feel free to make use of my code, I think it uses the same licence as the standard library.

[dylanede]

Right, I've got all of those test cases passing now by using blockOnMeta, except test₁₀, which is not something expected to work since this tactic does not have the magic coercion that @nad's tactic does, and test₁₈. Note that a small variation on test₁₈ does work:

  test₁₈ :
    (subst′ :
       ∀ {a p} {A : Set a} {x y : A}
       (P : A → Set p) → x ≡ y → P x → P y) →
    (∀ {a p} {A : Set a} {x : A} (P : A → Set p) (p : P x) →
     subst′ P refl p ≡ p) →
    (P : ℕ → Set)
    (f : ∀ {n} → P n → P n)
    (p : P 0) →
    f ⌞ subst′ P refl p ⌟ ≡ f p
  test₁₈ _ subst′-refl P _ _ = ⌊⌋ lhs (subst′-refl P _)

The difference is that the P argument to subst'-refl is no longer left to be inferred. The original version of test₁₈ gives these unsolved metavariables:

_1064 : f₁ ⌞ subst′ P refl p ⌟ ≡ f₁ p  [ at Tests.agda:127,32-55 ]
_y_1068 : _P_1073 _x_1072  [ at Tests.agda:127,32-34 ]
_a_1069 : Agda.Primitive.Level  [ at Tests.agda:127,40-51 ]
_A_1071 : Set _a_1069  [ at Tests.agda:127,40-51 ]
_x_1072 : _A_1071  [ at Tests.agda:127,40-51 ]
_P_1073 : _A_1071 → Set  [ at Tests.agda:127,52-53 ]

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  _y_1068 = p : P 0
  subst′ _P_1073 refl _y_1068 = subst′ P refl p : P 0
  _P_1073 _x_1072 =< P 0

I have tested providing everything apart from P (including all implicit arguments), which results in

_1064 : f ⌞ subst′ P refl p ⌟ ≡ f p  [ at Tests.agda:127,32-75 ]
_y_1068 : _P_1069 0  [ at Tests.agda:127,32-34 ]
_P_1069 : ℕ → Set (# 0)  [ at Tests.agda:127,72-73 ]

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  _y_1068 = p : P 0
  subst′ _P_1069 refl _y_1068 = subst′ P refl p : P 0
  _P_1069 0 =< P 0
  P 0 =< _P_1069 0

So it really is hinging on P.

[nad]

I tried to figure out why my tactic is slow, and this led me to report some problems related to blockOnMeta: agda/agda#4593, agda/agda#4594.

[nad]

I could make the tactic run faster in some cases by blocking on the last meta-variable instead of the first one. If the last meta-variable is solved after the first one, then this approach might lead to fewer invocations of the tactic.

[MatthewDaggitt]

Right, I've got all of those test cases passing now by using blockOnMeta

That's great news! One of the cases that I'm really interested in is using setoid rather than propositional equality. I think you mentioned that it worked for that, but I can't see one added yet. Does the following work?

module _ (S : CommutativeSemigroup a l) where
  open CommutativeSemigroup S
  open import Relation.Binary.Reasoning.Setoid setoid

  qu : (a b c d : ℤ) → a + b + c ≈ b + (a + c)
  qu a b c d  a+b+c≤d = begin
    ⌊ a + b ⌋ + c ≈⌊ +-comm a b ⌋
    b + a + c     ≈⟨ +-assoc b a c ⟩
    b + (a + c)   ∎
  

[nad]

Oh, I see now that you mean that you mean that your tactic implicitly handles sym-ifying terms and applying metavariables. Personally I am not yet sold on introducing that level of magic.

Applying the term to meta-variables is unproblematic if the term's type can be inferred, but there is no guarantee that the meta-variables will be solved. For sym I use backtracking, I can see why one might not want to do that. When everything works I think it is nice to be able to write things like by associativity instead of by (associativity x y z).

[MatthewDaggitt]

I think that there is something to be said for notation that doesn't steal the show here. They should be unintrusive because you're just trying to read a term whose meaning is not affected by the hole marks. In an on-paper proof you wouldn't mark the whole at all and most and usually you can still easily spot where the rewriting occurs.

Hmm I can definitely see your point @ajrouvoet. What are other people's thoughts? Is it better to be unobtrusive and closer to pen-and-paper or is it better to make it clearer what's going on?

[JacquesCarette]

Personally, I don't think this is a valid X or Y question. I think there are contexts in which each is useful.

For example, I think that the standard library should use a clear (if sometimes verbose) style. Proofs meant for users to read, i.e. where users are the primary audience of the proof, then closer to pen-and-paper is advantageous.

In other words, I suggest having 2 (sub)modules, with the user having a choice of which to use.

There is definitely a question of choosing a default, as it is unfair to ask everyone to have to make a choice [as too many won't have the necessary information to be able to make it.] I don't have strong opinions there. I slightly lean towards the one with more-magic-included as the default, as that will please beginners, and experts ought to know how to select alternate modules. Beginners tend to worry less about efficiency (as they are still in learning mode), but should be informed that 'magic' is not free.

[nad]

I have a tactic which infers the context automatically. This one tends to be slower and to fail more often, but when it works one gets away with zero annotations.

[nad]

Right, I've got all of those test cases passing now by using blockOnMeta, except […] test₁₈.

My code handles test₁₈, at the expense of test₁, by generating "cong _ _ f proof" rather than "cong lhs rhs f proof".

[dylanede]

That's great news! One of the cases that I'm really interested in is using setoid rather than propositional equality. I think you mentioned that it worked for that, but I can't see one added yet. Does the following work? ...

The problem with Setoid is that it doesn't come with a general congruence rule, i.e. ∀ f x y → x ≈ y → f x ≈ f y. And in fact, this is often not possible for many equivalence relations _≈_. It can however be proven for many individual instances of f, and is for example provided by isMagma instances for binary operations. agda-holes had begun down a path that would eventually automate use of these individual instances by letting the user provide a "database" of congruences the tactic can use. I purposefully left that out for this particular PR, as that is a lot of work. The macro would need to identify all of the operations that the hole is embedded in and construct a chain of calls to the various congruence rules. You would also typically want to allow congruence rules to be provided on the fly, for example for local function definitions, and I'm not sure how best to allow that (I think abusing instance search could get most of the way there though).

Note that once such a "database" feature exists, it should be possible to have a simple function that turns a CommutativeSemigroup instance (for example) into such a database by extracting the magmas, so it would still be simple to use the macro.

[dylanede]

In other words, I suggest having 2 (sub)modules, with the user having a choice of which to use.

@JacquesCarette , surely all that is needed is for the user to rename ⌊_⌋ and friends when importing them? Or do you mean one module with magic and one without, rather than the notation issue @MatthewDaggitt and @ajrouvoet were talking about?

[dylanede]

I have a tactic which infers the context automatically. This one tends to be slower and to fail more often, but when it works one gets away with zero annotations.

@nad, does that rely on the two sides of the relation having very similar structure, so that you can spot the relevant differences between them?

[JacquesCarette]

I mean one module with magic and one without. Magic is fragile and can have hard-to-predict computational cost.

[dylanede]

The more I think about it, the more I think that instance search would be the ideal solution for the "database" of congruences. So as long as you had an instance of congruence for a given function in scope with respect to the equivalence relation, the (theoretical) macro would be able to find it for each function it encounters and use it to build up the required chain.

[JacquesCarette]

It is indeed the ideal kind of magic...

[nad]

@nad, does that rely on the two sides of the relation having very similar structure, so that you can spot the relevant differences between them?

Yes.

[nad]

Here is another test case that fails:

{-# OPTIONS --cubical #-}

open import Agda.Builtin.Cubical.Path

postulate
  cong  : ∀ {a b} {A : Set a} {B : Set b}
          (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
  trans : ∀ {a} {A : Set a} {x y z : A} → x ≡ y → y ≡ z → x ≡ z

infix  -1 finally
infixr -2 _≡⟨⟩_

_≡⟨⟩_ : ∀ {a} {A : Set a} (x {y} : A) → x ≡ y → x ≡ y
_ ≡⟨⟩ x≡y = x≡y

finally : ∀ {a} {A : Set a} (x y : A) → x ≡ y → x ≡ y
finally _ _ x≡y = x≡y

syntax finally x y x≡y = x ≡⟨ x≡y ⟩∎ y ∎

open import Tactic.Cong.Common
open import Tactic.Cong 2 _≡_ cong ℓSet projₗ projₛ _≡_ trans

record R (F : Set → Set) : Set₁ where
  field
    p : {A : Set} {x : F A} → x ≡ x

open R ⦃ … ⦄ public

test :
  {F : Set → Set} ⦃ r : R F ⦄ {A : Set} {x₁ x₂ : F A}
  (p₁ p₂ : x₁ ≡ x₂) (assumption : p₁ ≡ p₂) →
  trans p p₁ ≡ trans p p₂
test p₁ p₂ assumption =
  trans p p₁      ≡⟨⟩
  trans p ⌞ p₁ ⌟  ≡⟨ ⌊⌋ lhs assumption ⟩∎
  trans p p₂      ∎

See agda/agda#4067.

[MatthewDaggitt]

Closing as superseded by #1658 (although it is not quite as generic as this proposal).