From 5b7d25727d110836f44daf61a38397fe8a58fb9c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 Mar 2020 06:35:42 -0700
Subject: [PATCH] doc: matcher for values example

---
 tmp/eqns/matchVal.lean | 47 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 tmp/eqns/matchVal.lean

diff --git a/tmp/eqns/matchVal.lean b/tmp/eqns/matchVal.lean
new file mode 100644
index 0000000000..0e70647396
--- /dev/null
+++ b/tmp/eqns/matchVal.lean
@@ -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₂