From 54213b48dc3a4b63c1afffdd2071343caf40d4fe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 11 Nov 2014 00:29:21 -0800
Subject: [PATCH] feat(library/data/prod/wf): lex of well-founded relations is
 well-founded

---
 library/data/prod/wf.lean | 48 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)
 create mode 100644 library/data/prod/wf.lean

diff --git a/library/data/prod/wf.lean b/library/data/prod/wf.lean
new file mode 100644
index 000000000..92b6b0a6c
--- /dev/null
+++ b/library/data/prod/wf.lean
@@ -0,0 +1,48 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+import data.prod.decl logic.wf
+open well_founded
+
+namespace prod
+  section
+  variables {A B : Type}
+  variable  (Ra  : A → A → Prop)
+  variable  (Rb  : B → B → Prop)
+
+  inductive lex : A × B → A × B → Prop :=
+  left  : ∀a₁ b₁ a₂ b₂, Ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂),
+  right : ∀a b₁ b₂,     Rb b₁ b₂ → lex (a, b₁)  (a, b₂)
+  end
+
+  context
+  parameters {A B : Type}
+  parameters {Ra  : A → A → Prop} {Rb  : B → B → Prop}
+  infix `≺`:50 := lex Ra Rb
+
+  definition accessible {a} (aca : acc Ra a) (acb : ∀b, acc Rb b): ∀b, acc (lex Ra Rb) (a, b) :=
+  acc.rec_on aca
+    (λxa aca (iHa : ∀y, Ra y xa → ∀b, acc (lex Ra Rb) (y, b)),
+      λb, acc.rec_on (acb b)
+        (λxb acb
+          (iHb : ∀y, Rb y xb → acc (lex Ra Rb) (xa, y)),
+          acc.intro (xa, xb) (λp (lt : p ≺ (xa, xb)),
+            have aux : xa = xa → xb = xb → acc (lex Ra Rb) p, from
+              @lex.rec_on A B Ra Rb (λp₁ p₂, pr₁ p₂ = xa → pr₂ p₂ = xb → acc (lex Ra Rb) p₁)
+                         p (xa, xb) lt
+                (λa₁ b₁ a₂ b₂ (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ = xb),
+                  show acc (lex Ra Rb) (a₁, b₁), from
+                  have Ra₁  : Ra a₁ xa, from eq.rec_on eq₂ H,
+                  iHa a₁ Ra₁ b₁)
+                (λa b₁ b₂ (H : Rb b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ = xb),
+                  show acc (lex Ra Rb) (a, b₁), from
+                  have Rb₁  : Rb b₁ xb, from eq.rec_on eq₃ H,
+                  eq.rec_on (eq.symm eq₂) (iHb b₁ Rb₁)),
+            aux rfl rfl)))
+
+  -- The lexicographical order of well founded relations is well-founded
+  definition wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (lex Ra Rb) :=
+  well_founded.intro (λp, destruct p (λa b, accessible (Ha a) (well_founded.apply Hb) b))
+
+  end
+end prod