From aedfb5be2c02989f6500bb6fdc87d756d0b1e92f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 30 Aug 2013 16:34:41 -0700 Subject: [PATCH] Add another example that demonstrates how to use implicit arguments Signed-off-by: Leonardo de Moura --- examples/ex15.lean | 47 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 examples/ex15.lean diff --git a/examples/ex15.lean b/examples/ex15.lean new file mode 100644 index 0000000000..ad1756535d --- /dev/null +++ b/examples/ex15.lean @@ -0,0 +1,47 @@ + +Variable N : Type +Variable h : N -> N -> N + +Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := + Congr (Congr (Refl h) H1) H2 + +(* Display the theorem showing implicit arguments *) +Set lean::pp::implicit true +Show Environment 2 + +(* Display the theorem hiding implicit arguments *) +Set lean::pp::implicit false +Show Environment 2 + +Theorem Example1 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) := + DisjCases H + (fun H1 : a = b ∧ b = c, + CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) + (fun H1 : a = d ∧ d = c, + CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) + +(* Show proof of the last theorem with all implicit arguments *) +Set lean::pp::implicit true +Show Environment 1 + +(* Using placeholders to hide the type of H1 *) +Theorem Example2 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) := + DisjCases H + (fun H1 : _, + CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) + (fun H1 : _, + CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) + +Set lean::pp::implicit true +Show Environment 1 + +(* Same example but the first conjuct has unnecessary stuff *) +Theorem Example3 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) := + DisjCases H + (fun H1 : _, + CongrH (Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))) (Refl b)) + (fun H1 : _, + CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) + +Set lean::pp::implicit false +Show Environment 1