8038604d3e
This adds the concept of **functional induction** to lean. Derived from the definition of a (possibly mutually) recursive function, a **functional induction principle** is tailored to proofs about that function. For example from: ``` def ackermann : Nat → Nat → Nat | 0, m => m + 1 | n+1, 0 => ackermann n 1 | n+1, m+1 => ackermann n (ackermann (n + 1) m) derive_functional_induction ackermann ``` we get ``` ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0) (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m)) (x x : Nat) : motive x x ``` At the moment, the user has to ask for the functional induction principle explicitly using ``` derive_functional_induction ackermann ``` The module docstring of `Lean/Meta/Tactic/FunInd.lean` contains more details on the design and implementation of this command. More convenience around this (e.g. a `functional induction` tactic) will follow eventually. This PR includes a bunch of `PSum`/`PSigma` related functions in the `Lean.Tactic.FunInd` namespace. I plan to move these to `PackArgs`/`PackMutual` afterwards, and do some cleaning up as I do that. --------- Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk> Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
100 lines
3.7 KiB
Text
100 lines
3.7 KiB
Text
import Lean.Elab.Tactic.Guard
|
||
|
||
inductive Expr where
|
||
| nat : Nat → Expr
|
||
| plus : Expr → Expr → Expr
|
||
| bool : Bool → Expr
|
||
| and : Expr → Expr → Expr
|
||
|
||
inductive Ty where
|
||
| nat
|
||
| bool
|
||
deriving DecidableEq
|
||
|
||
inductive HasType : Expr → Ty → Prop
|
||
| nat : HasType (.nat v) .nat
|
||
| plus : HasType a .nat → HasType b .nat → HasType (.plus a b) .nat
|
||
| bool : HasType (.bool v) .bool
|
||
| and : HasType a .bool → HasType b .bool → HasType (.and a b) .bool
|
||
|
||
theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by
|
||
cases h₁ <;> cases h₂ <;> rfl
|
||
|
||
inductive Maybe (p : α → Prop) where
|
||
| found : (a : α) → p a → Maybe p
|
||
| unknown
|
||
|
||
notation "{{ " x " | " p " }}" => Maybe (fun x => p)
|
||
|
||
def Expr.typeCheck (e : Expr) : {{ ty | HasType e ty }} :=
|
||
match e with
|
||
| nat .. => .found .nat .nat
|
||
| bool .. => .found .bool .bool
|
||
| plus a b =>
|
||
match a.typeCheck, b.typeCheck with
|
||
| .found .nat h₁, .found .nat h₂ => .found .nat (.plus h₁ h₂)
|
||
| _, _ => .unknown
|
||
| and a b =>
|
||
match a.typeCheck, b.typeCheck with
|
||
| .found .bool h₁, .found .bool h₂ => .found .bool (.and h₁ h₂)
|
||
| _, _ => .unknown
|
||
termination_by e
|
||
|
||
theorem Expr.typeCheck_correct (h₁ : HasType e ty) (h₂ : e.typeCheck ≠ .unknown)
|
||
: e.typeCheck = .found ty h := by
|
||
revert h₂
|
||
cases typeCheck e with
|
||
| found ty' h' => intro; have := HasType.det h₁ h'; subst this; rfl
|
||
| unknown => intros; contradiction
|
||
|
||
derive_functional_induction Expr.typeCheck
|
||
|
||
/--
|
||
info: Expr.typeCheck.induct (motive : Expr → Prop) (case1 : ∀ (a : Nat), motive (Expr.nat a))
|
||
(case2 : ∀ (a : Bool), motive (Expr.bool a))
|
||
(case3 :
|
||
∀ (a b : Expr) (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat),
|
||
Expr.typeCheck b = Maybe.found Ty.nat h₂ →
|
||
Expr.typeCheck a = Maybe.found Ty.nat h₁ → motive a → motive b → motive (Expr.plus a b))
|
||
(case4 :
|
||
∀ (a b : Expr),
|
||
(∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat),
|
||
Expr.typeCheck a = Maybe.found Ty.nat h₁ → Expr.typeCheck b = Maybe.found Ty.nat h₂ → False) →
|
||
motive a → motive b → motive (Expr.plus a b))
|
||
(case5 :
|
||
∀ (a b : Expr) (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
|
||
Expr.typeCheck b = Maybe.found Ty.bool h₂ →
|
||
Expr.typeCheck a = Maybe.found Ty.bool h₁ → motive a → motive b → motive (Expr.and a b))
|
||
(case6 :
|
||
∀ (a b : Expr),
|
||
(∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
|
||
Expr.typeCheck a = Maybe.found Ty.bool h₁ → Expr.typeCheck b = Maybe.found Ty.bool h₂ → False) →
|
||
motive a → motive b → motive (Expr.and a b))
|
||
(x : Expr) : motive x
|
||
-/
|
||
#guard_msgs in
|
||
#check Expr.typeCheck.induct
|
||
|
||
/-
|
||
This no longer works after splitting non-refining tail-call matches,
|
||
as we now have different number of variables
|
||
|
||
theorem Expr.typeCheck_complete {e : Expr} : e.typeCheck = .unknown → ¬ HasType e ty := by
|
||
apply Expr.typeCheck.induct (motive := fun e => e.typeCheck = .unknown → ¬ HasType e ty)
|
||
<;> simp [typeCheck]
|
||
<;> {
|
||
intro _ _ a b iha ihb
|
||
split <;> simp [*]
|
||
intro ht; cases ht
|
||
next hnp h₁ h₂ => exact hnp h₁ h₂ (typeCheck_correct h₁ (iha · h₁)) (typeCheck_correct h₂ (ihb · h₂))
|
||
}
|
||
-/
|
||
|
||
-- The same, using the induction tactic
|
||
theorem Expr.typeCheck_complete' {e : Expr} : e.typeCheck = .unknown → ¬ HasType e ty := by
|
||
induction e using Expr.typeCheck.induct
|
||
all_goals simp [typeCheck]
|
||
case case3 | case5 => simp [*]
|
||
case case4 iha ihb | case6 iha ihb =>
|
||
intro ht; cases ht
|
||
next hnp h₁ h₂ => exact hnp h₁ h₂ (typeCheck_correct h₁ (iha · h₁)) (typeCheck_correct h₂ (ihb · h₂))
|