98 lines
3.6 KiB
Text
98 lines
3.6 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
|
||
|
||
/--
|
||
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),
|
||
b.typeCheck = Maybe.found Ty.nat h₂ →
|
||
a.typeCheck = Maybe.found Ty.nat h₁ → motive a → motive b → motive (a.plus b))
|
||
(case4 :
|
||
∀ (a b : Expr),
|
||
(∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat),
|
||
a.typeCheck = Maybe.found Ty.nat h₁ → b.typeCheck = Maybe.found Ty.nat h₂ → False) →
|
||
motive a → motive b → motive (a.plus b))
|
||
(case5 :
|
||
∀ (a b : Expr) (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
|
||
b.typeCheck = Maybe.found Ty.bool h₂ →
|
||
a.typeCheck = Maybe.found Ty.bool h₁ → motive a → motive b → motive (a.and b))
|
||
(case6 :
|
||
∀ (a b : Expr),
|
||
(∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
|
||
a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → False) →
|
||
motive a → motive b → motive (a.and b))
|
||
(e : Expr) : motive e
|
||
-/
|
||
#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 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₂))
|