From a8c3322ac8f4e282641bc3cd897587d337ebe841 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Mar 2020 16:46:31 -0700 Subject: [PATCH] doc: expand dependent pattern matching support for array literals --- src/Init/Data/Array/Basic.lean | 4 +- src/Init/Data/Nat/Basic.lean | 3 + tmp/eqns/matchArrayLit.lean | 184 ++++++++++++++++++++++++++++++++- 3 files changed, 184 insertions(+), 7 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index b525060f0f..c3cf42b35d 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -97,8 +97,8 @@ def getOp [Inhabited α] (self : Array α) (idx : Nat) : α := self.get! idx -- auxiliary declaration used in the equation compiler when pattern matching array literals. -abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : n = a.size) (h₂ : i < n) : α := -a.get ⟨i, h₁ ▸ h₂⟩ +abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α := +a.get ⟨i, h₁.symm ▸ h₂⟩ @[extern "lean_array_fset"] def set (a : Array α) (i : @& Fin a.size) (v : α) : Array α := diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 901674de3d..9f806d907a 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -349,6 +349,9 @@ theorem subLt : ∀ {n m : Nat}, 0 < n → 0 < m → n - m < n protected theorem ltOfLtOfLe {n m k : Nat} : n < m → m ≤ k → n < k := Nat.leTrans +protected theorem ltOfLtOfEq {n m k : Nat} : n < m → m = k → n < k := +fun h₁ h₂ => h₂ ▸ h₁ + protected theorem leOfEq {n m : Nat} (p : n = m) : n ≤ m := p ▸ Nat.leRefl n diff --git a/tmp/eqns/matchArrayLit.lean b/tmp/eqns/matchArrayLit.lean index e10948c144..595064e576 100644 --- a/tmp/eqns/matchArrayLit.lean +++ b/tmp/eqns/matchArrayLit.lean @@ -1,5 +1,6 @@ -universes u +universes u v +namespace Experiment1 inductive ArrayLitMatch (α : Type u) | sz0 {} : ArrayLitMatch | sz1 (a₁ : α) : ArrayLitMatch @@ -8,13 +9,13 @@ inductive ArrayLitMatch (α : Type u) | other {} : ArrayLitMatch def matchArrayLit {α : Type u} (a : Array α) : ArrayLitMatch α := -if 0 = a.size then +if a.size = 0 then ArrayLitMatch.sz0 -else if h : 1 = a.size then +else if h : a.size = 1 then ArrayLitMatch.sz1 (a.getLit 0 h (ofDecideEqTrue rfl)) -else if h : 2 = a.size then +else if h : a.size = 2 then ArrayLitMatch.sz2 (a.getLit 0 h (ofDecideEqTrue rfl)) (a.getLit 1 h (ofDecideEqTrue rfl)) -else if h : 3 = a.size then +else if h : a.size = 3 then ArrayLitMatch.sz3 (a.getLit 0 h (ofDecideEqTrue rfl)) (a.getLit 1 h (ofDecideEqTrue rfl)) (a.getLit 2 h (ofDecideEqTrue rfl)) else ArrayLitMatch.other @@ -33,3 +34,176 @@ rfl def matchArrayLit.eq4 {α : Type u} (a₁ a₂ a₃ a₄ : α) : matchArrayLit #[a₁, a₂, a₃, a₄] = ArrayLitMatch.other := rfl +end Experiment1 + +theorem Array.ext {α : Type u} (a b : Array α) : a.size = b.size → (∀ (i : Nat) (hi₁ : i < a.size) (hi₂ : i < b.size) , a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩) → a = b := +match a, b with +| ⟨sz₁, f₁⟩, ⟨sz₂, f₂⟩ => + show sz₁ = sz₂ → (∀ (i : Nat) (hi₁ : i < sz₁) (hi₂ : i < sz₂) , f₁ ⟨i, hi₁⟩ = f₂ ⟨i, hi₂⟩) → Array.mk sz₁ f₁ = Array.mk sz₂ f₂ from + fun h₁ h₂ => + match sz₁, sz₂, f₁, f₂, h₁, h₂ with + | sz, _, f₁, f₂, rfl, h₂ => + have f₁ = f₂ from funext $ fun ⟨i, hi₁⟩ => h₂ i hi₁ hi₁; + congrArg _ this + +theorem Array.extLit {α : Type u} {n : Nat} + (a b : Array α) + (hsz₁ : a.size = n) (hsz₂ : b.size = n) + (h : ∀ (i : Nat) (hi : i < n), a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b := +Array.ext a b (hsz₁.trans hsz₂.symm) $ fun i hi₁ hi₂ => h i (hsz₁ ▸ hi₁) + +def toListLitAux {α : Type u} (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i ≤ a.size → List α → List α +| 0, hi, acc => acc +| (i+1), hi, acc => toListLitAux i (Nat.leOfSuccLe hi) (a.getLit i hsz (Nat.ltOfLtOfEq (Nat.ltOfLtOfLe (Nat.ltSuccSelf i) hi) hsz) :: acc) + +def toArrayLit {α : Type u} (a : Array α) (n : Nat) (hsz : a.size = n) : Array α := +List.toArray $ toListLitAux a n hsz n (hsz ▸ Nat.leRefl _) [] + +theorem toArrayLitEq {α : Type u} (a : Array α) (n : Nat) (hsz : a.size = n) : a = toArrayLit a n hsz := +-- TODO: this is painful to prove without proper automation +sorry +/- +First, we need to prove +∀ i j acc, i ≤ a.size → (toListLitAux a n hsz (i+1) hi acc).index j = if j < i then a.getLit j hsz _ else acc.index (j - i) +by induction + +Base case is trivial +(j : Nat) (acc : List α) (hi : 0 ≤ a.size) + |- (toListLitAux a n hsz 0 hi acc).index j = if j < 0 then a.getLit j hsz _ else acc.index (j - 0) +... |- acc.index j = acc.index j + +Induction + +(j : Nat) (acc : List α) (hi : i+1 ≤ a.size) + |- (toListLitAux a n hsz (i+1) hi acc).index j = if j < i + 1 then a.getLit j hsz _ else acc.index (j - (i + 1)) + ... |- (toListLitAux a n hsz i hi' (a.getLit i hsz _ :: acc)).index j = if j < i + 1 then a.getLit j hsz _ else acc.index (j - (i + 1)) * by def + ... |- if j < i then a.getLit j hsz _ else (a.getLit i hsz _ :: acc).index (j-i) * by induction hypothesis + = + if j < i + 1 then a.getLit j hsz _ else acc.index (j - (i + 1)) +If j < i, then both are a.getLit j hsz _ +If j = i, then lhs reduces else-branch to (a.getLit i hsz _) and rhs is then-brachn (a.getLit i hsz _) +If j >= i + 1, we use + - j - i >= 1 > 0 + - (a::as).index k = as.index (k-1) If k > 0 + - j - (i + 1) = (j - i) - 1 + Then lhs = (a.getLit i hsz _ :: acc).index (j-i) = acc.index (j-i-1) = acc.index (j-(i+1)) = rhs + +With this proof, we have + +∀ j, j < n → (toListLitAux a n hsz n _ []).index j = a.getLit j hsz _ + +We also need + +- (toListLitAux a n hsz n _ []).length = n +- j < n -> (List.toArray as).getLit j _ _ = as.index j + +Then using Array.extLit, we have that a = List.toArray $ toListLitAux a n hsz n _ [] +-/ + +theorem Array.eqLitOfSize0 {α : Type u} (a : Array α) (hsz : a.size = 0) : a = #[] := +toArrayLitEq a 0 hsz +/- +Array.ext a #[] h (fun i h₁ h₂ => absurd h₂ (Nat.notLtZero _)) +-/ + +theorem Array.eqLitOfSize1 {α : Type u} (a : Array α) (hsz : a.size = 1) : a = #[a.getLit 0 hsz (ofDecideEqTrue rfl)] := +toArrayLitEq a 1 hsz +/- +Array.extLit a #[a.getLit 0 hsz (ofDecideEqTrue rfl)] hsz rfl $ fun i => + match i with + | 0 => fun hi => rfl + | (n+1) => fun hi => + have n < 0 from hi; + absurd this (Nat.notLtZero _) +-/ + +theorem Array.eqLitOfSize2 {α : Type u} (a : Array α) (hsz : a.size = 2) : a = #[a.getLit 0 hsz (ofDecideEqTrue rfl), a.getLit 1 hsz (ofDecideEqTrue rfl)] := +toArrayLitEq a 2 hsz +/- +Array.extLit a #[a.getLit 0 hsz (ofDecideEqTrue rfl), a.getLit 1 hsz (ofDecideEqTrue rfl)] hsz rfl $ fun i => + match i with + | 0 => fun hi => rfl + | 1 => fun hi => rfl + | (n+2) => fun hi => + have n < 0 from hi; + absurd this (Nat.notLtZero _) +-/ + +theorem Array.eqLitOfSize3 {α : Type u} (a : Array α) (hsz : a.size = 3) : + a = #[a.getLit 0 hsz (ofDecideEqTrue rfl), a.getLit 1 hsz (ofDecideEqTrue rfl), a.getLit 2 hsz (ofDecideEqTrue rfl)] := +toArrayLitEq a 3 hsz +/- +Array.extLit a #[a.getLit 0 hsz (ofDecideEqTrue rfl), a.getLit 1 hsz (ofDecideEqTrue rfl), a.getLit 2 hsz (ofDecideEqTrue rfl)] hsz rfl $ fun i => + match i with + | 0 => fun hi => rfl + | 1 => fun hi => rfl + | 2 => fun hi => rfl + | (n+3) => fun hi => + have n < 0 from hi; + absurd this (Nat.notLtZero _) +-/ + +/- +Matcher for the following patterns +``` +| #[] => _ +| #[a₁] => _ +| #[a₁, a₂, a₃] => _ +| a => _ +``` -/ +def matchArrayLit {α : Type u} (C : Array α → Sort v) (a : Array α) + (h₁ : Unit → C #[]) + (h₂ : ∀ a₁, C #[a₁]) + (h₃ : ∀ a₁ a₂ a₃, C #[a₁, a₂, a₃]) + (h₄ : ∀ a, C a) + : C a := +if h : a.size = 0 then + @Eq.ndrec _ _ C (h₁ ()) _ (toArrayLitEq a 0 h).symm +else if h : a.size = 1 then + @Eq.ndrec _ _ C (h₂ (a.getLit 0 h (ofDecideEqTrue rfl))) _ (toArrayLitEq a 1 h).symm +else if h : a.size = 3 then + @Eq.ndrec _ _ C (h₃ (a.getLit 0 h (ofDecideEqTrue rfl)) (a.getLit 1 h (ofDecideEqTrue rfl)) (a.getLit 2 h (ofDecideEqTrue rfl))) _ (toArrayLitEq a 3 h).symm +else + h₄ a + +/- Equational lemmas that should be generated automatically. -/ +theorem matchArrayLit.eq1 {α : Type u} (C : Array α → Sort v) + (h₁ : Unit → C #[]) + (h₂ : ∀ a₁, C #[a₁]) + (h₃ : ∀ a₁ a₂ a₃, C #[a₁, a₂, a₃]) + (h₄ : ∀ a, C a) + : matchArrayLit C #[] h₁ h₂ h₃ h₄ = h₁ () := +rfl + +theorem matchArrayLit.eq2 {α : Type u} (C : Array α → Sort v) + (h₁ : Unit → C #[]) + (h₂ : ∀ a₁, C #[a₁]) + (h₃ : ∀ a₁ a₂ a₃, C #[a₁, a₂, a₃]) + (h₄ : ∀ a, C a) + (a₁ : α) + : matchArrayLit C #[a₁] h₁ h₂ h₃ h₄ = h₂ a₁ := +rfl + +theorem matchArrayLit.eq3 {α : Type u} (C : Array α → Sort v) + (h₁ : Unit → C #[]) + (h₂ : ∀ a₁, C #[a₁]) + (h₃ : ∀ a₁ a₂ a₃, C #[a₁, a₂, a₃]) + (h₄ : ∀ a, C a) + (a₁ a₂ a₃ : α) + : matchArrayLit C #[a₁, a₂, a₃] h₁ h₂ h₃ h₄ = h₃ a₁ a₂ a₃ := +rfl + +theorem matchArrayLit.eq4 {α : Type u} (C : Array α → Sort v) + (h₁ : Unit → C #[]) + (h₂ : ∀ a₁, C #[a₁]) + (h₃ : ∀ a₁ a₂ a₃, C #[a₁, a₂, a₃]) + (h₄ : ∀ a, C a) + (a : Array α) + (n₁ : a.size ≠ 0) (n₂ : a.size ≠ 1) (n₃ : a.size ≠ 3) + : matchArrayLit C a h₁ h₂ h₃ h₄ = h₄ a := +match a, n₁, n₂, n₃ with +| ⟨0, _⟩, n₁, _, _ => absurd rfl n₁ +| ⟨1, _⟩, _, n₂, _ => absurd rfl n₂ +| ⟨2, _⟩, _, _, _ => rfl +| ⟨3, _⟩, _, _, n₃ => absurd rfl n₃ +| ⟨n+4, _⟩, _, _, _ => rfl