From e1f591ba61bb7a6d85dea7f353063ab138d908d2 Mon Sep 17 00:00:00 2001 From: Daniel Fabian Date: Mon, 27 Sep 2021 14:06:21 +0000 Subject: [PATCH] test: do no use unit in ac_expr.lean. It is not necessary to define a unit element for the proof to go through. --- tests/lean/run/ac_expr.lean | 70 ++++++++++++++++++++----------------- 1 file changed, 37 insertions(+), 33 deletions(-) diff --git a/tests/lean/run/ac_expr.lean b/tests/lean/run/ac_expr.lean index 9ce7c25cd4..0829efab62 100644 --- a/tests/lean/run/ac_expr.lean +++ b/tests/lean/run/ac_expr.lean @@ -1,18 +1,24 @@ import Std -inductive Expr where - | var (i : Nat) - | op (lhs rhs : Expr) - deriving Inhabited, Repr +inductive Expr (maxVarId : Nat) : Type where + | var (i : Fin maxVarId) + | op (lhs rhs : Expr maxVarId) + deriving Repr -def List.getIdx : List α → Nat → α → α - | [], i, u => u - | a::as, 0, u => a - | a::as, i+1, u => getIdx as i u +def List.getIdx : (l : List α) → Fin l.length → α + | [], ⟨_, i⟩ => by + simp [length] at i + apply absurd i + cases i + | a::as, ⟨0, _⟩ => a + | a::as, ⟨i+1, h⟩ => by + apply getIdx as ⟨i, _⟩ + simp [List.length_cons] at h + apply Nat.lt_of_succ_lt_succ + assumption structure Context (α : Type u) where op : α → α → α - unit : α assoc : (a b c : α) → op (op a b) c = op a (op b c) comm : (a b : α) → op a b = op b a vars : List α @@ -20,50 +26,50 @@ structure Context (α : Type u) where theorem Context.left_comm (ctx : Context α) (a b c : α) : ctx.op a (ctx.op b c) = ctx.op b (ctx.op a c) := by rw [← ctx.assoc, ctx.comm a b, ctx.assoc] -def Expr.denote (ctx : Context α) : Expr → α +def Expr.denote (ctx : Context α) : Expr ctx.vars.length → α | Expr.op a b => ctx.op (denote ctx a) (denote ctx b) - | Expr.var i => ctx.vars.getIdx i ctx.unit + | Expr.var i => ctx.vars.getIdx i -theorem Expr.denote_op (ctx : Context α) (a b : Expr) : denote ctx (Expr.op a b) = ctx.op (denote ctx a) (denote ctx b) := +theorem Expr.denote_op (ctx : Context α) (a b : Expr ctx.vars.length) : denote ctx (Expr.op a b) = ctx.op (denote ctx a) (denote ctx b) := rfl -def Expr.concat : Expr → Expr → Expr +def Expr.concat : Expr n → Expr n → Expr n | Expr.op a b, c => Expr.op a (concat b c) | Expr.var i, c => Expr.op (Expr.var i) c -theorem Expr.denote_concat (ctx : Context α) (a b : Expr) : denote ctx (concat a b) = denote ctx (Expr.op a b) := by +theorem Expr.denote_concat (ctx : Context α) (a b : Expr ctx.vars.length) : denote ctx (concat a b) = denote ctx (Expr.op a b) := by induction a with | var i => rfl | op _ _ _ ih => simp [denote, ih, ctx.assoc] -def Expr.flat : Expr → Expr +def Expr.flat : Expr n → Expr n | Expr.op a b => concat (flat a) (flat b) | Expr.var i => Expr.var i -theorem Expr.denote_flat (ctx : Context α) (e : Expr) : denote ctx (flat e) = denote ctx e := by +theorem Expr.denote_flat (ctx : Context α) (e : Expr ctx.vars.length) : denote ctx (flat e) = denote ctx e := by induction e with | var i => rfl | op a b ih₁ ih₂ => simp [flat, denote, denote_concat, ih₁, ih₂] -theorem Expr.eq_of_flat (ctx : Context α) (a b : Expr) (h : flat a = flat b) : denote ctx a = denote ctx b := by +theorem Expr.eq_of_flat (ctx : Context α) (a b : Expr ctx.vars.length) (h : flat a = flat b) : denote ctx a = denote ctx b := by have h := congrArg (denote ctx) h simp [denote_flat] at h assumption -def Expr.length : Expr → Nat +def Expr.length : Expr n → Nat | op a b => 1 + b.length | _ => 1 -def Expr.sort (e : Expr) : Expr := +def Expr.sort (e : Expr n) : Expr n := loop e.length e where - loop : Nat → Expr → Expr + loop : Nat → Expr n → Expr n | fuel+1, Expr.op a e => let (e₁, e₂) := swap a e Expr.op e₁ (loop fuel e₂) | _, e => e - swap : Expr → Expr → Expr × Expr + swap : Expr n → Expr n → Expr n × Expr n | Expr.var i, Expr.op (Expr.var j) e => if i > j then let (e₁, e₂) := swap (Expr.var j) e @@ -78,10 +84,10 @@ where (Expr.var i, Expr.var j) | e₁, e₂ => (e₁, e₂) -theorem Expr.denote_sort (ctx : Context α) (e : Expr) : denote ctx (sort e) = denote ctx e := by +theorem Expr.denote_sort (ctx : Context α) (e : Expr ctx.vars.length) : denote ctx (sort e) = denote ctx e := by apply denote_loop where - denote_loop (n : Nat) (e : Expr) : denote ctx (sort.loop n e) = denote ctx e := by + denote_loop (n : Nat) (e : Expr ctx.vars.length) : denote ctx (sort.loop n e) = denote ctx e := by induction n generalizing e with | zero => rfl | succ n ih => @@ -97,7 +103,7 @@ where simp [denote, ih] assumption - denote_swap (e₁ e₂ : Expr) : denote ctx (Expr.op (sort.swap e₁ e₂).1 (sort.swap e₁ e₂).2) = denote ctx (Expr.op e₁ e₂) := by + denote_swap (e₁ e₂ : Expr ctx.vars.length) : denote ctx (Expr.op (sort.swap e₁ e₂).1 (sort.swap e₁ e₂).2) = denote ctx (Expr.op e₁ e₂) := by induction e₂ generalizing e₁ with | op a b ih' ih => clear ih' @@ -128,7 +134,7 @@ where focus simp [sort.swap, h] | _ => rfl -theorem Expr.eq_of_sort_flat (ctx : Context α) (a b : Expr) (h : sort (flat a) = sort (flat b)) : denote ctx a = denote ctx b := by +theorem Expr.eq_of_sort_flat (ctx : Context α) (a b : Expr ctx.vars.length) (h : sort (flat a) = sort (flat b)) : denote ctx a = denote ctx b := by have h := congrArg (denote ctx) h simp [denote_flat, denote_sort] at h assumption @@ -138,21 +144,19 @@ theorem ex₁ (x₁ x₂ x₃ x₄ : Nat) : (x₁ + x₂) + (x₃ + x₄) = x₁ { op := Nat.add assoc := Nat.add_assoc comm := Nat.add_comm - unit := Nat.zero vars := [x₁, x₂, x₃, x₄] } - (Expr.op (Expr.op (Expr.var 0) (Expr.var 1)) (Expr.op (Expr.var 2) (Expr.var 3))) - (Expr.op (Expr.op (Expr.op (Expr.var 0) (Expr.var 1)) (Expr.var 2)) (Expr.var 3)) - rfl + (Expr.op (Expr.op (Expr.var ⟨0, by simp⟩) (Expr.var ⟨1, by simp⟩)) (Expr.op (Expr.var ⟨2, by simp⟩) (Expr.var ⟨3, by simp⟩))) + (Expr.op (Expr.op (Expr.op (Expr.var ⟨0, by simp⟩) (Expr.var ⟨1, by simp⟩)) (Expr.var ⟨2, by simp⟩)) (Expr.var ⟨3, by simp⟩)) + (by rfl) theorem ex₂ (x₁ x₂ x₃ x₄ : Nat) : (x₁ + x₂) + (x₃ + x₄) = x₃ + x₁ + x₂ + x₄ := Expr.eq_of_sort_flat { op := Nat.add assoc := Nat.add_assoc comm := Nat.add_comm - unit := Nat.zero vars := [x₁, x₂, x₃, x₄] } - (Expr.op (Expr.op (Expr.var 0) (Expr.var 1)) (Expr.op (Expr.var 2) (Expr.var 3))) - (Expr.op (Expr.op (Expr.op (Expr.var 2) (Expr.var 0)) (Expr.var 1)) (Expr.var 3)) - rfl + (Expr.op (Expr.op (Expr.var ⟨0, by simp⟩) (Expr.var ⟨1, by simp⟩)) (Expr.op (Expr.var ⟨2, by simp⟩) (Expr.var ⟨3, by simp⟩))) + (Expr.op (Expr.op (Expr.op (Expr.var ⟨2, by simp⟩) (Expr.var ⟨0, by simp⟩)) (Expr.var ⟨1, by simp⟩)) (Expr.var ⟨3, by simp⟩)) + (by rfl) #print ex₂