193 lines
7.4 KiB
Text
193 lines
7.4 KiB
Text
universes u v
|
||
|
||
namespace Experiment1
|
||
inductive ArrayLitMatch (α : Type u)
|
||
| sz0 {} : ArrayLitMatch
|
||
| sz1 (a₁ : α) : ArrayLitMatch
|
||
| sz2 (a₁ a₂ : α) : ArrayLitMatch
|
||
| sz3 (a₁ a₂ a₃ : α) : ArrayLitMatch
|
||
| other {} : ArrayLitMatch
|
||
|
||
def matchArrayLit {α : Type u} (a : Array α) : ArrayLitMatch α :=
|
||
if a.size = 0 then
|
||
ArrayLitMatch.sz0
|
||
else if h : a.size = 1 then
|
||
ArrayLitMatch.sz1 (a.getLit 0 h (ofDecideEqTrue rfl))
|
||
else if h : a.size = 2 then
|
||
ArrayLitMatch.sz2 (a.getLit 0 h (ofDecideEqTrue rfl)) (a.getLit 1 h (ofDecideEqTrue rfl))
|
||
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
|
||
|
||
def matchArrayLit.eq0 {α : Type u} : matchArrayLit (#[] : Array α) = ArrayLitMatch.sz0 :=
|
||
rfl
|
||
|
||
def matchArrayLit.eq1 {α : Type u} (a₁ : α) : matchArrayLit #[a₁] = ArrayLitMatch.sz1 a₁ :=
|
||
rfl
|
||
|
||
def matchArrayLit.eq2 {α : Type u} (a₁ a₂ : α) : matchArrayLit #[a₁, a₂] = ArrayLitMatch.sz2 a₁ a₂ :=
|
||
rfl
|
||
|
||
def matchArrayLit.eq3 {α : Type u} (a₁ a₂ a₃ : α) : matchArrayLit #[a₁, a₂, a₃] = ArrayLitMatch.sz3 a₁ a₂ a₃ :=
|
||
rfl
|
||
|
||
def matchArrayLit.eq4 {α : Type u} (a₁ a₂ a₃ a₄ : α) : matchArrayLit #[a₁, a₂, a₃, a₄] = ArrayLitMatch.other :=
|
||
rfl
|
||
end Experiment1
|
||
|
||
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.rec _ _ (fun x _ => C x) (h₁ ()) _ (toArrayLitEq a 0 h).symm
|
||
else if h : a.size = 1 then
|
||
@Eq.rec _ _ (fun x _ => C x) (h₂ (a.getLit 0 h (ofDecideEqTrue rfl))) _ (toArrayLitEq a 1 h).symm
|
||
else if h : a.size = 3 then
|
||
@Eq.rec _ _ (fun x _ => C x) (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
|