doc: expand dependent pattern matching support for array literals
This commit is contained in:
Leonardo de Moura
parent
3a94422aea
commit
a8c3322ac8
3 changed files with 184 additions and 7 deletions
|
|
@ -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 α :=
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue