d39b0415f0
Sets the default value to `pp.fieldNotation.generalized` to `true`. Updates tests, and fixes some minor flaws in the implementation of the generalized field notation pretty printer. Now generalized field notation won't be used for any function that has a `motive` argument. This is intended to prevent recursors from pretty printing using it as (1) recursors are more like control flow structures than actual functions and (2) generalized field notation tends to cause elaboration problems for recursors. Note: be sure functions that have an `@[app_unexpander]` use `@[pp_nodot]` if applicable. For example, `List.toArray` needs `@[pp_nodot]` to ensure the unexpander prints it using `#[...]` notation.
100 lines
3.6 KiB
Text
100 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
|
||
|
||
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),
|
||
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))
|
||
(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₂))
|