Add new goal and hypothesis at the same time

Stream: new members

[Gabriel Alfour]

Hi, still new to Lean4.

I have a hypothesis h : A -> B, in tactic mode, I'd like to write something like pose (h _), this should:

• Create a new goal / proof obligation for A
• After this new goal / proof obligation is performed, add B to the hypotheses

If there's no equivalent, I'd like to know what is an equivalent to assert A in Coq. ChatGPT gives me old syntax, and I still haven't found a guide of "Lean4 for the old Coq-er"

Thanks!

[Gabriel Alfour]

I have found the equivalent of assert A, which is have _ : A := show ...!
I am still looking for something like pose (h _)

[Eric Wieser]

I think that's just have := h ?_

[Gabriel Alfour]

@Eric Wieser nice, thx! Is there an equivalent that reverses the two goals? (So that I have to prove the implicit obligation from ?_ first?)

[Yaël Dillies]

Yes, it's suffices

[Gabriel Alfour]

@Yaël Dillies I'm sorry, I don't get it. What is the equivalent of have h_applied := h ?_ with suffices?

[Notification Bot]

This topic was moved here from #general > Add new goal and hypothesis at the same time by Kyle Miller.

[Kyle Miller]

@Gabriel Alfour Something we like around here to ground questions is an #mwe -- if you can create a little examples to accompany your questions that set up some sort of context that illustrates what you're talking about, then people can fill it in with a concrete suggestion.

[Gabriel Alfour]

@Kyle Miller sgtm

I tried to share from the Lean4 Editor, but the URL is unwieldy, should I just copy-paste the code like so?

inductive ast : Type
| Lam : String -> ast -> ast
| Var : String -> ast
| App : ast -> ast -> ast


-- rewriting
inductive rewrite_step_result : Type
| Finish
| Next : ast -> rewrite_step_result

open ast
open rewrite_step_result

def substitute (expr : ast) (var : String) (sub : ast) :=
  match expr with
  | Var var' => if var = var' then sub else Var var'
  | App f arg => App (substitute f var sub) (substitute arg var sub)
  | Lam var' body => if var = var' then Lam var' body else Lam var' (substitute body var sub)

def rewrite_step : ast -> rewrite_step_result
  | Var _var => Finish
  | Lam _var _body => Finish
  | App f arg => (
    match rewrite_step f with
    | Finish => (
      match rewrite_step arg with
      | Finish => (
        match f with
        | Lam var body => Next (substitute body var arg)
        | _ => Finish
      )
      | Next arg' => Next (App f arg')
    )
    | Next f' => Next (App f' arg)
  )

def is_normal (expr : ast) := rewrite_step expr = Finish

open Nat
def rewrite_n_steps (expr : ast) (n : Nat) :=
  match n with
  | zero => Next expr
  | succ n' => (
    match rewrite_step expr with
    | Finish => Finish
    | Next expr' => rewrite_n_steps expr' n'
  )

def terminates (expr : ast) := ∃ n , rewrite_n_steps expr n = Finish

def looper : ast :=
  App (Lam "x" (App (Var "x") (Var "x"))) (Lam "x" (App (Var "x") (Var "x")))

theorem looper_loops : rewrite_n_steps looper 1 = Next looper :=
  by
  eq_refl

theorem looper_loops_forever : forall n , rewrite_n_steps looper n = Next looper :=
  by
  intro n
  induction n with
  | zero => eq_refl
  | succ _ ih =>
    exact ih

theorem non_terminating : ∃ (expr : ast) , ¬terminates expr :=
  by
  exists looper
  unfold terminates
  intro tl
  let ⟨ n , ih ⟩ := tl
  have ih' : (rewrite_n_steps looper n = Next looper) := looper_loops_forever n
  rw [ih] at ih'
  contradiction

namespace Typed

  inductive type : Type
  | Nat
  | Fun : type -> type -> type
  deriving DecidableEq

  inductive tast : Type
  | TVar : String -> tast
  | TApp : tast -> tast -> tast
  | TLam : String -> type -> tast -> tast

  open tast
  def remove_types : tast -> ast
  | TLam v _ty body => Lam v (remove_types body)
  | TVar v => Var v
  | TApp f arg => App (remove_types f) (remove_types arg)

  namespace Typecheck

    inductive result : Type
    | Fail
    | Succeed : type -> result

    def context : Type := List (String × type)

    open result
    open type
    def main (ctx : context) : tast -> result
    | TVar v => (
      match List.lookup v ctx with
      | none => Fail
      | some ty => Succeed ty
    )
    | TLam v ty body => (
      let ctx := List.cons (v , ty) ctx
      main ctx body
    )
    | TApp f arg => (
      match main ctx arg with
      | Fail => Fail
      | Succeed arg_ty => (
        match main ctx f with
        | Fail => Fail
        | Succeed f' => (
          match f' with
          | Fun in_ty out_ty => (
            if in_ty = arg_ty then Succeed out_ty
            else Fail
          )
          | _ => Fail
        )
      )
    )

  end Typecheck

  open Typecheck

  theorem stlc_terminate :
    ∀ (ctx : context) (tast : tast) (ty : type) ,
      main ctx tast = result.Succeed ty -> ∃ n ,
      rewrite_n_steps (remove_types tast) n = Finish :=
  by
    intros ctx tast ty success
    induction tast
    . exists 1
    . rename_i f arg f_ih arg_ih
      -- in the following line, I'd like the two goals generated to be reversed
      have f_ih_r := f_ih ?_
      . admit
      . unfold main at success
        --- This is where in Coq, I would do `destruct (main ctx arg)`, and it would get rewritten in all assumptions


end Typed

[Kyle Miller]

Code blocks like that are preferred. There's even a web editor link in the upper-right corner.

[Kyle Miller]

One feature you might use here are named metavariables:

      have f_ih_r := f_ih ?g
      case g =>
        unfold main at success
      sorry

[Kyle Miller]

(Lean tradition is to use sorry to apologize for not being done yet rather than using admit to concede the argument :smile:)

[Kyle Miller]

You can also swap the goals

[Gabriel Alfour]

@Kyle Miller Thanks!

[Gabriel Alfour]

@Kyle Miller swap is not recognized

[Gabriel Alfour]

and can't find it online

[Eric Wieser]

You'll need import Mathlib.Tactic, though probably there's a smaller file you could import

[Martin Dvořák]

import Mathlib.Tactic.PermuteGoals

[Richard Copley]

Or Mathlib.Tactic.Common.

This file imports all tactics which do not have significant theory imports,
and hence can be imported very low in the theory import hierarchy,
thereby making tactics widely available without needing specific imports.

So, including it in user code is not exactly what it is meant for, but one can argue that user code that does not have many imports is also "low in the theory import hierarchy".