max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: matcher for values example

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-13 06:35:42 -07:00
parent 04f071606f
commit 5b7d25727d
1 changed files with 47 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
tmp/eqns/matchVal.lean Normal file
View file

@ -0,0 +1,47 @@
universes v
/-
matcher for the following patterns
```
| "hello" => _
| "world" => _
| a => _
``` -/
def matchString (C : String → Sort v) (s : String)
(h₁ : Unit → C "hello")
(h₂ : Unit → C "world")
(h₃ : ∀ s, C s)
: C s :=
if h : s = "hello" then
@Eq.rec _ _ (fun x _ => C x) (h₁ ()) _ h.symm
else if h : s = "world" then
@Eq.rec _ _ (fun x _ => C x) (h₂ ()) _ h.symm
else
h₃ s
theorem matchString.Eq1 (C : String → Sort v)
(h₁ : Unit → C "hello")
(h₂ : Unit → C "world")
(h₃ : ∀ s, C s)
: matchString C "hello" h₁ h₂ h₃ = h₁ () :=
ifPos rfl
axiom neg1 : "world" ≠ "hello"
theorem matchString.Eq2 (C : String → Sort v)
(h₁ : Unit → C "hello")
(h₂ : Unit → C "world")
(h₃ : ∀ s, C s)
: matchString C "world" h₁ h₂ h₃ = h₂ () :=
have aux₁ : matchString C "world" h₁ h₂ h₃ = if h : "world" = "world" then @Eq.rec _ _ (fun x _ => C x) (h₂ ()) _ h.symm else h₃ "world" from difNeg neg1;
have aux₂ : (if h : "world" = "world" then @Eq.rec _ _ (fun x _ => C x) (h₂ ()) _ h.symm else h₃ "world" : C "world") = h₂ () from difPos rfl;
Eq.trans aux₁ aux₂
theorem matchString.Eq3 (C : String → Sort v)
(h₁ : Unit → C "hello")
(h₂ : Unit → C "world")
(h₃ : ∀ s, C s)
(s : String) (n₁ : s ≠ "hello") (n₂ : s ≠ "world")
: matchString C s h₁ h₂ h₃ = h₃ s :=
have aux₁ : matchString C s h₁ h₂ h₃ = if h : s = "world" then @Eq.rec _ _ (fun x _ => C x) (h₂ ()) _ h.symm else h₃ s from difNeg n₁;
have aux₂ : (if h : s = "world" then @Eq.rec _ _ (fun x _ => C x) (h₂ ()) _ h.symm else h₃ s : C s) = h₃ s from difNeg n₂;
Eq.trans aux₁ aux₂