If and match in conv mode

Stream: lean4

[Tomas Skrivan]

I have almost managed to implement if <condition> then <convSeq on true> else <convSeq on false> notation for conv mode.

I'm not quire there as I have to write if <condition> | <goal> then <convSeq on true> else <convSeq on false> i.e. I have to specify the whole goal | <goal>. This is because I internally call a rewrite on the whole goal: rw [convIf_id <condition> <goal>].

So I have two questions:

1. What would be the easiest way to get rid of the necessity of specifying the goal?
2. What would it take to implement match notation: match <term> with | <ctor 1> => <convSeq1> ... ? That is probably much, much harder. I do not even know where would I start.

Working example:

opaque foo : Int → Int
axiom foo.pos (x : Int) (h : x ≥ 0) : foo x =  1
axiom foo.neg (x : Int) (h : ¬(x ≥ 0)) : foo x = -1

@[inline]
abbrev convIf {α} (P : Prop) (_ : Decidable P) (x : P → α) (y : ¬P → α) : α := if h : P then x h else y h

theorem convIf_id {α} (P : Prop) [inst : Decidable P] (a : α) : a = convIf P inst (λ _ => a) (λ _ => a) :=
by
  simp[convIf]; cases inst; rename_i q; simp[q]; rename_i q; simp[q]; done


open Lean.Parser.Tactic.Conv
syntax "if" ident ":" term "|" term "then" convSeq "else" convSeq : conv
macro_rules
| `(conv| if $h : $P | $t then $trueConv else $falseConv) =>
  `(convSeq| rw [convIf_id $P $t]
             conv => enter[3]; intro $h; ($trueConv)
             conv => enter[4]; intro $h; ($falseConv))


example : foo = λ (x : Int) => if x ≥ 0 then 1 else -1 :=
by

  conv =>
    lhs; enter [x]

    if h : x ≥ 0 | (foo x) then
      rw [foo.pos x h]
    else
      rw [foo.neg x h]

  done

[Tomas Skrivan]

If anyone is interested I have managed to get if ... then ... else ... notation in conv working.

import Lean

@[inline]
abbrev convIf {α} (P : Prop) (_ : Decidable P) (x : P → α) (y : ¬P → α) : α := if h : P then x h else y h

def convIf.rhs {α} (P : Prop) [inst : Decidable P] (a : α) := convIf P inst (λ _ => a) (λ _ => a)

theorem convIf.id {α} (P : Prop) [inst : Decidable P] (a : α) : a = convIf P inst (λ _ => a) (λ _ => a) :=
by
  simp[convIf]; cases inst; rename_i q; simp[q]; rename_i q; simp[q]; done

open Lean.Parser.Tactic.Conv
syntax (name := conv_if) "if" ident ":" term  "then" convSeq "else" convSeq : conv

open Lean.Elab Tactic Conv in
@[tactic conv_if]
def convIfTactic : Tactic
| `(conv| if $h : $P then $trueConv else $falseConv) => do
   withMainContext do

     let p ← elabTerm P none
     let t' ← Lean.Meta.mkAppM ``convIf.rhs #[p, (← getLhs)]
     let h' ← Lean.Meta.mkAppM ``convIf.id  #[p, (← getLhs)]

     updateLhs t' h'
     evalTactic (←
       `(convSeq| unfold convIf.rhs
                  conv => enter[3]; intro $h; ($trueConv)
                  conv => enter[4]; intro $h; ($falseConv)))
| _ => throwUnsupportedSyntax

opaque foo : Int → Int
axiom foo.pos (x : Int) (h : x ≥ 0) : foo x =  1
axiom foo.neg (x : Int) (h : ¬(x ≥ 0)) : foo x = -1

example : foo = λ (x : Int) => if x ≥ 0 then 1 else -1 :=
by

  conv =>
    lhs; enter [x]

    if h : x ≥ 0 then
      rw [foo.pos x h]
    else
      rw [foo.neg x h]

  done

[Jeremy Salwen]

Thank you I needed this!