Improving this syntax

Stream: lean4

[François G. Dorais]

After another mostly unrelated discussion, I remembered that I had been using a custom by_cases tactic. Here is my current code:

syntax by_cases_true := "|" &"isTrue" (ident <|> "_") "=>" (hole <|> syntheticHole <|> tacticSeq)
syntax by_cases_false := "|" &"isFalse" (ident <|> "_") "=>" (hole <|> syntheticHole <|> tacticSeq)
syntax "by_cases" term "with" withPosition((colGe by_cases_true) (colGe by_cases_false)) : tactic
macro_rules
| `(tactic|by_cases $p with | isTrue $ht => $tt | isFalse $hf => $tf) =>
  `(tactic|match inferInstanceAs (Decidable $p) with | Decidable.isTrue $ht => $tt | Decidable.isFalse $hf => $tf)

My main idea was to use a match-style syntax to allow me to use different identifiers in the true/false cases, whereas the built-in by_cases forces the same identifier in both cases. (As an unintended bonus, this version of by_cases actually checks whether the proposition is decidable and the built-in version does not.)

There is an obvious defect to this code where I'm forced to write the cases in the true then false order. I think I know how to fix that. But what I really want and couldn't find a way to make it work is to allow by_cases to apply to several propositions. For example, I would want to write:

by_cases p, q, r with
| ifTrue hp, ifTrue hq, ifTrue hr => ...
| ifTrue _, ifTrue hq, ifFalse hnr => ...
| ifTrue _, ifFalse hnq, ifTrue _ => ...
| ifTrue hp, ifFalse hnq, ifFalse _ => ...
| ifFalse hnp, ifTrue hq, ifTrue hr => ...
| ifFalse hnp, ifTrue hq, ifFalse hnr => ...
| ifFalse hnp, ifFalse _, ifTrue hr => ...
| ifFalse hnp, ifFalse hnq, ifFalse hnr => ...

I gave up after a couple of headaches. Maybe someone with more expertise knows how to do this? (Bonus points if the cases can be in any order.)

[Jannis Limperg]

I would try to do this one syntactically: transform

by_cases x, y, ... with

=>

match decide x, decide y, ... with

and use the regular syntax for match alternatives for the cases.

[Mario Carneiro]

macro (name := byCases) "by_cases" ps:term,* "with" alts:Lean.Parser.Tactic.matchAlts : tactic =>
  `(tactic| match $[inferInstanceAs (Decidable $ps)],* with $alts:matchAlts)

example : True := by
  by_cases 1 < 2, 3 < 4 with
  | isTrue h1, isTrue h2 => trivial
  | isTrue h1, isFalse h2 => trivial
  | isFalse h1, isTrue h2 => trivial
  | isFalse h1, isFalse h2 => trivial

[François G. Dorais]

You rock Mario!

It looks simpler but I don't think your idea works Jannis; how do I get case-by-case identifiers that way?

[François G. Dorais]

I guess $[...] is way more powerful than I thought. Does it do some kind of automatic folding? I don't really get how $[inferInstanceAs (Decidable $ps)],* actually works. I'll have to mull it over for a bit...

[Jannis Limperg]

François G. Dorais said:

It looks simpler but I don't think your idea works Jannis; how do I get case-by-case identifiers that way?

I meant exactly what Mario did, only with more fuzziness. ;)

[Mario Carneiro]

François G. Dorais said:

I guess $[...] is way more powerful than I thought. Does it do some kind of automatic folding? I don't really get how $[inferInstanceAs (Decidable $ps)],* actually works. I'll have to mull it over for a bit...

You can look at the generated code for syntax quotations by doing stuff like

open Lean Syntax in
#check fun ps alts => `(tactic| match $[inferInstanceAs (Decidable $ps)],* with $alts:matchAlts)

fun ps alts => do
  let info ← MonadRef.mkInfoFromRefPos
  let scp ← getCurrMacroScope
  let mainModule ← getMainModule
  pure
      (node SourceInfo.none `Lean.Parser.Tactic.match
        #[atom info "match", node SourceInfo.none `null #[], node SourceInfo.none `null #[],
          node SourceInfo.none `null
            (Array.append #[]
              (mkSepArray
                (Array.map -- map here
                  (fun ps =>
                    node SourceInfo.none `Lean.Parser.Term.matchDiscr
                      #[node SourceInfo.none `null #[],
                        node SourceInfo.none `Lean.Parser.Term.app
                          #[ident info (String.toSubstring "inferInstanceAs")
                              (addMacroScope mainModule `inferInstanceAs scp) [(`inferInstanceAs, [])],
                            node SourceInfo.none `null
                              #[node SourceInfo.none `Lean.Parser.Term.paren
                                  #[atom info "(",
                                    node SourceInfo.none `null
                                      #[node SourceInfo.none `Lean.Parser.Term.app
                                          #[ident info (String.toSubstring "Decidable")
                                              (addMacroScope mainModule `Decidable scp) [(`Decidable, [])],
                                            node SourceInfo.none `null #[ps]], --insert ps into the tree
                                        node SourceInfo.none `null #[]],
                                    atom info ")"]]]])
                  ps) -- the actual `Array Syntax` input
                (mkAtom ","))),
          atom info "with", alts]) : (ps : Array Syntax) → (alts : Syntax) → ?m.1001 ps alts Syntax

You have to squint a bit to see what it's doing, but you can see the Array.map in there

[Yuri de Wit]

TIL: #check ...