Potential for a cong helper macro in Tactic module

[dylanede]

agda-holes is a library that makes working with cong more convenient and succinct. This issue is for discussing the possibility of adding some similar functionality inside the Tactic module alongside the ring and monoid solvers.

agda-holes is not usable as-is. It has bit-rotted from the current stable Agda, and it also relies on uses of the TERMINATING pragma, which would presumably need to be removed and the corresponding functions refactored. It would also need to be made properly agnostic over cong implementations (e.g. from cubical Agda). I might be interested in undertaking the work to make it suitable for inclusion when I get some time, so I'm interested in whether this sounds like a good idea.

[gallais]

This would be a very nice addition. :)

[dylanede]

agda-holes auto-applies sym if necessary. I'm not sold on that idea myself as I prefer explicit yet DRY code. Thoughts?

Also, the exact syntax is up for bikeshedding. One possibility is that it becomes an alternative form of _≡⟨_⟩_, instead of a separate call, or both forms could be available.

[dylanede]

I quite like the idea of using _≡⌞⟨_⟩⌟_, to stress that you are operating inside the "hole". A line of a proof might then look like this:

⌞ (b + c) + a * b ⌟ + a * c     ≡⌞⟨ +-assoc b c (a * b) ⟩⌟

[JacquesCarette]

That would be a very nice addition.

Opinions:

1. I would prefer _≡⌞⌟⟨_⟩_ over _≡⌞⟨_⟩⌟_
2. I also prefer to be explicit in my uses of sym.

[dylanede]

OK, I think I prefer that too, so how does this sound?

1. _≡⌞⌟⟨_⟩_ for use in equational reasoning
   2.⌞⌟ as a standalone function-like macro, e.g. ⌞⌟ $ +-assoc b c (a * b)

This second form would be convenient for use in single line proofs, where the ⌞_⌟ wrapped part is part of the signature of the proof. It could be a prefix operator instead to remove the common need for $, but that might make readability suffer.

If we had a defaultTo tactic as alluded to in an example in the Agda documentation, importing the cong macros could be done as follows:

open import Tactic.Holes

would use cong from the standard library, but

open import Tactic.Holes {{mycong}}

would use a different, user-specified implementation.

[ajrouvoet]

Although visually the proposed syntax is fine, I am a little worried about how much effort it takes to input, and that comes from someone who is completely sold on the unicode front :)

Why not either _≡⌞_⌟_ or _≡⌊_⌋_ if you want to or have to distinguish them from the usual infix reasoning combinators?

[JacquesCarette]

Oh, I like those suggestions! Especially the first one. [Sometimes it takes a bad syntax suggestion to prod someone else to have a better one... yeah, I'll go with that! ;) ]

[gallais]

@ajrouvoet's suggestion would make it nicely compatible with the ˘ symbol to
combine sym & automation.

[ajrouvoet]

the ˘ symbol

Talking about syntax, the categories library had the much nicer IMO _↑≡⟨_⟩_ and _↓≡⟨_⟩_ to indicate the direction of the equality. But perhaps that ship has sailed :)

[MatthewDaggitt]

Just to add my voice that this would be a great idea! I like the _≡⌊_⌋_ syntax best myself, but _≡⌞_⌟_ is also good (it's just the brackets are a little low compared to all the other brackets we use).

Talking about syntax, the categories library had the much nicer IMO ↑≡⟨⟩_ and ↓≡⟨⟩_ to indicate the direction of the equality. But perhaps that ship has sailed :)

@ajrouvoet I too would like to do something about the ˘ syntax, even though I introduced it (@JacquesCarette I can definitely relate!). I really hate it: it's difficult to type, it ruins the alignment of proofs and doesn't clearly convey symmetry to me. Perhaps you could open a separate issue in which we could come up with an alternative?

[JacquesCarette]

And now issue #1138 seems to have been introduced for discussing just that. We should keep the discussion here about cong-helper.

[dylanede]

Just a heads up: I'm writing my own implementation, not based on agda-holes. I have the implementation of ⌊_⌋ with ⌊⌋ working, i.e. code like this works:

foo : (a b c : ℤ) → ⌊ a + b ⌋ + c ≡ b + a + c
foo a b c = ⌊⌋ (+-comm a b)

This should also work with the ⌊_⌋ nested deep within lambdas, though it needs more testing to be sure.

It is currently proving a bit tricky to write the _≡⌊_⌋_ form, due to a combination of quote ⌊⌋ not being able to find ⌊⌋ (quote: not a defined name) for some reason, and the type checker being a bit too eager to normalise terms. I am making progress however.

The code is sitting at 139 lines in a single file. It is being tested against cong from the standard library at the moment. I expect that in order to make it cope with cong from, say, agda/cubical, I will need something like an application routine (see agda/agda#3821 for some relevant discussion). This will make the code a bit larger, but I do not see it becoming as complex as agda-holes. It is also fully --safe.

[dylanede]

Hmmph.

Even with

foo2 : (a b c : ℤ) → ⌊ a + b ⌋ + c ≡ b + a + c
foo2 a b c = begin
  ⌊ a + b ⌋ + c ≡⟨ ⌊⌋ (+-comm a b) ⟩
  b + a + c ∎

the type of the term given to the ⌊⌋ macro has already been normalised to a + b + c ≡ b + a + c, removing the hole annotation. Not sure what I can do about that. Presumably this is behaviour in the compiler introduced in the time since agda-holes was written.

[dylanede]

Sorry to spam, but I fixed that problem with the normalisation - adding

{-# NOINLINE ⌊_⌋ #-}

stopped the eager normalisation.

[dylanede]

And now _≡⌊_⌋_ works. 🎉
Before I submit a PR I will try to get it to work with cubical's cong as well.

[dylanede]

To help visualise possible syntax, here's a slightly more complex proof that works with the new macro:

Note that default font rendering on GitHub does not maintain fixed width glyphs - view this in Emacs for best results

foo : (a b c d : ℤ) → (a + b) * (c + d) ≡ a * c + a * d + b * c + b * d
foo a b c d = begin
  (a + b) * (c + d)                   ≡⟨ *-distribˡ-+ (a + b) _ _ ⟩
  ⌊ (a + b) * c ⌋ + (a + b) * d       ≡⌊ *-distribʳ-+ c a b ⌋
  a * c + b * c + ⌊ (a + b) * d ⌋     ≡⌊ *-distribʳ-+ d a b ⌋
  a * c + b * c + (a * d + b * d)     ≡⟨ +-assoc (a * c) _ _  ⟩
  a * c + ⌊ b * c + (a * d + b * d)⌋  ≡⌊ +-comm (b * c) _ ⌋
  a * c + ((a * d + b * d) + b * c)   ≡⟨ sym $ +-assoc (a * c) _ _ ⟩
  ⌊ a * c + (a * d + b * d) ⌋ + b * c ≡⌊ sym $ +-assoc (a * c) _ _ ⌋
  a * c + a * d + b * d + b * c       ≡⟨ +-assoc (a * c + a * d) _ _ ⟩
  a * c + a * d + ⌊ b * d + b * c ⌋   ≡⌊ +-comm (b * d) _ ⌋
  a * c + a * d + (b * c + b * d)     ≡⟨ sym $ +-assoc (a * c + a * d) _ _ ⟩
  a * c + a * d + b * c + b * d       ∎

I have chosen ⌊ and ⌋ over ⌞ and ⌟ for the time being, though that's completely up for debate.

[dylanede]

In order to be generic over more cong implementations, I need a more generic way of applying Terms to each other. For this purpose I have written the below code, however I have yet to get this to satisfy the termination checker. Any help would be appreciated.

{-# OPTIONS --without-K --safe #-}

open import Reflection
open import Reflection.Term
open import Reflection.Argument
open import Function.Base
open import Data.List
open import Data.Nat

failed-apply : Term → Arg Term → TC Term
failed-apply t (arg _ a) = typeError $ strErr "Attempted to apply" ∷ termErr a ∷ strErr "to" ∷ termErr t ∷ []

apply : Arg Term → Term → TC Term
subst : ℕ → Term → Term → TC Term
subst-args : ℕ → Term → List (Arg Term) → TC (List (Arg Term))

apply a (var x args) = return $ var x (args ∷ʳ a)
apply a (con c args) = return $ con c (args ∷ʳ a)
apply a (def f args) = return $ def f (args ∷ʳ a)
apply a (meta x args) = return $ meta x (args ∷ʳ a)
-- TODO: irrelevant arguments are not handled yet - not sure how to
apply (vArg x) (vLam _ t) = subst 0 x t
apply (hArg x) (hLam _ t) = subst 0 x t
apply (iArg x) (iLam _ t) = subst 0 x t
-- TODO - pattern lambdas and pi terms
apply a (pat-lam cs args) =  typeError $ strErr "TODO" ∷ []
apply a (pi _ _) = typeError $ strErr "TODO" ∷ []
apply a t = failed-apply t a -- catch all

subst i x (var j args)        with compare i j
...                              | less m k = do -- decrement j by one since λ was eliminated
                                   args ← subst-args i x args
                                   return $ var (m + k) args -- j ≡ suc (m + k)
...                              | greater _ _ = do -- j refers to variable inside eliminated λ
                                   args ← subst-args i x args
                                   return $ var j args
subst i x (var j [])             | equal _ = return x
subst i x (var j (arg v a ∷ as)) | equal _ = do
                                   a′ ← subst i x a
                                   xa ← apply (arg v a′) x
                                   subst i xa (var j as)
subst i x (con c args) = do
  args ← subst-args i x args
  return $ con c args
subst i x (def f args) = do
  args ← subst-args i x args
  return $ def f args
subst i x (lam v (abs s t)) = do
  t ← subst (suc i) x t
  return $ lam v (abs s t)
subst i x (meta m args) = do
  args ← subst-args i x args
  return $ meta m args
subst i x (sort s) = return $ sort s
subst i x (lit l) = return $ lit l
subst i x unknown = return unknown
subst i x (pat-lam cs args) = typeError $ strErr "TODO" ∷ []
subst i x (pi a b) = typeError $ strErr "TODO" ∷ []

subst-args i x [] = return []
subst-args i x (arg v a ∷ as) = do
  a ← subst i x a
  as ← subst-args i x as
  return $ arg v a ∷ as

[jespercockx]

In general substitution of terms is not terminating since reflected terms are untyped. You might want to take a look at https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Reflection/Substitute.agda for a way to define a safe version of substitution (and application) that is terminating.

[dylanede]

That safe version looks ideal for my purposes, thanks! It looks like something that would be very useful to have in the standard library.

[dylanede]

I'm a little concerned by UlfNorell/agda-prelude#65 however.

[MatthewDaggitt]

It looks like something that would be very useful to have in the standard library.

Yup, agreed. If you've after you've had a fiddle with it, we'd definitely appreciate you opening a pull request 😄

[dylanede]

Heads up: I now have it working with cong from Cubical Agda as well. I've stuck with (better versions of) my own apply and substitute functions. I am working around the termination problem by making the maximum number of recursive apply calls a module parameter, which I think is practical for most use cases.

Before I make a PR, there are some things to take care of:

• Make it accept more implementations of the binary relation. It currently relies on the relation being a definition somewhere (not, e.g. a lambda). Fixing this properly will effectively require a restricted "unapply" function, which again would be generally useful in other tactics.
• Move the apply/substitute/unapply machinery into its own module inside Reflection.
• Tie up some TODOs related to pattern lambdas
• Generally tidy things up
• Make a nice README module and move the tests into that.

From what I have learnt here it should be possible to make a "selective normalisation" function that would greatly help #1071.

[dylanede]

The PR is up (#1158).

[MatthewDaggitt]

An alternative proposal was added in #1658