diff --git a/library/logic/examples/propositional/deceq.lean b/library/logic/examples/propositional/deceq.lean
new file mode 100644
index 000000000..e998bf567
--- /dev/null
+++ b/library/logic/examples/propositional/deceq.lean
@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+
+PropF has decidable equality
+-/
+import .soundness
+open bool decidable nat
+
+namespace PropF
+  -- Show that PropF has decidable equality
+
+  definition equal : PropF → PropF → bool
+  | (Var x) (Var y)           := if x = y then tt else ff
+  | Bot Bot                   := tt
+  | (Conj p₁ p₂) (Conj q₁ q₂) := equal p₁ q₁ && equal p₂ q₂
+  | (Disj p₁ p₂) (Disj q₁ q₂) := equal p₁ q₁ && equal p₂ q₂
+  | (Impl p₁ p₂) (Impl q₁ q₂) := equal p₁ q₁ && equal p₂ q₂
+  | _            _            := ff
+
+  lemma equal_refl : ∀ p, equal p p = tt
+  | (Var x)      := if_pos rfl
+  | Bot          := rfl
+  | (Conj p₁ p₂) := begin change (equal p₁ p₁ && equal p₂ p₂ = tt), rewrite *equal_refl end
+  | (Disj p₁ p₂) := begin change (equal p₁ p₁ && equal p₂ p₂ = tt), rewrite *equal_refl end
+  | (Impl p₁ p₂) := begin change (equal p₁ p₁ && equal p₂ p₂ = tt), rewrite *equal_refl end
+
+  lemma equal_to_eq : ∀ ⦃p q⦄, equal p q = tt → p = q
+  | (Var x) (Var y) H :=
+    if H₁ : x = y then congr_arg Var H₁
+    else by rewrite [▸ (if x = y then tt else ff) = tt at H, if_neg H₁ at H]; exact (absurd H ff_ne_tt)
+  | Bot Bot H  := rfl
+  | (Conj p₁ p₂) (Conj q₁ q₂) H :=
+    by rewrite [equal_to_eq (band_elim_left H), equal_to_eq (band_elim_right H)]
+  | (Disj p₁ p₂) (Disj q₁ q₂) H :=
+    by rewrite [equal_to_eq (band_elim_left H), equal_to_eq (band_elim_right H)]
+  | (Impl p₁ p₂) (Impl q₁ q₂) H :=
+    by rewrite [equal_to_eq (band_elim_left H), equal_to_eq (band_elim_right H)]
+
+  lemma has_decidable_eq [instance] : decidable_eq PropF :=
+  decidable_eq_of_bool_pred equal_to_eq equal_refl
+end PropF
diff --git a/library/logic/examples/propositional/soundness.lean b/library/logic/examples/propositional/soundness.lean
new file mode 100644
index 000000000..560abdec0
--- /dev/null
+++ b/library/logic/examples/propositional/soundness.lean
@@ -0,0 +1,165 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+
+Define propositional calculus, valuation, provability, validity, prove soundness.
+
+This file is based on Floris van Doorn Coq files.
+-/
+import data.nat data.list
+open nat bool list decidable
+
+definition PropVar [reducible] := nat
+
+inductive PropF :=
+| Var  : PropVar → PropF
+| Bot  : PropF
+| Conj : PropF → PropF → PropF
+| Disj : PropF → PropF → PropF
+| Impl : PropF → PropF → PropF
+
+namespace PropF
+  notation `#`:max P:max := Var P
+  notation A ∨ B         := Disj A B
+  notation A ∧ B         := Conj A B
+  infixr `⇒`:25          := Impl
+  notation `⊥`           := Bot
+
+  definition Neg A       := A ⇒ ⊥
+  notation ~ A           := Neg A
+  definition Top         := ~⊥
+  notation `⊤`           := Top
+  definition BiImpl A B  := A ⇒ B ∧ B ⇒ A
+  infixr `⇔`:25          := BiImpl
+
+  definition valuation   := PropVar → bool
+
+  definition TrueQ (v : valuation) : PropF → bool
+  | TrueQ (# P)   := v P
+  | TrueQ ⊥       := ff
+  | TrueQ (A ∨ B) := TrueQ A || TrueQ B
+  | TrueQ (A ∧ B) := TrueQ A && TrueQ B
+  | TrueQ (A ⇒ B) := bnot (TrueQ A) || TrueQ B
+
+  definition is_true [reducible] (b : bool) := b = tt
+
+  -- the valuation v satisfies a list of PropF, if forall (A : PropF) in Γ,
+  -- (TrueQ v A) is tt (the Boolean true)
+  definition Satisfies v Γ := ∀ A, A ∈ Γ → is_true (TrueQ v A)
+  definition Models Γ A    := ∀ v, Satisfies v Γ → is_true (TrueQ v A)
+
+  infix `⊨`:80 := Models
+
+  definition Valid p := [] ⊨ p
+  reserve infix `⊢`:80
+
+  /- Provability -/
+
+  inductive Nc : list PropF → PropF → Prop :=
+  infix ⊢ := Nc
+  | Nax   : ∀ Γ A,   A ∈ Γ →               Γ ⊢ A
+  | ImpI  : ∀ Γ A B, (A::Γ) ⊢ B →          Γ ⊢ (A ⇒ B)
+  | ImpE  : ∀ Γ A B, Γ ⊢ (A ⇒ B) → Γ ⊢ A → Γ ⊢ B
+  | BotC  : ∀ Γ A,   ((~A)::Γ) ⊢ ⊥       → Γ ⊢ A
+  | AndI  : ∀ Γ A B, Γ ⊢ A → Γ ⊢ B       → Γ ⊢ (A ∧ B)
+  | AndE₁ : ∀ Γ A B, Γ ⊢ (A ∧ B)         → Γ ⊢ A
+  | AndE₂ : ∀ Γ A B, Γ ⊢ (A ∧ B)         → Γ ⊢ B
+  | OrI₁  : ∀ Γ A B, Γ ⊢ A               → Γ ⊢ (A ∨ B)
+  | OrI₂  : ∀ Γ A B, Γ ⊢ B               → Γ ⊢ (A ∨ B)
+  | OrE   : ∀ Γ A B C, Γ ⊢ (A ∨ B) → (A :: Γ) ⊢ C → (B :: Γ) ⊢ C → Γ ⊢ C
+
+  infix ⊢ := Nc
+
+  definition Provable A := [] ⊢ A
+
+  definition Prop_Soundness := ∀ A, Provable A → Valid A
+
+  definition Prop_Completeness := ∀ A, Valid A → Provable A
+
+  open Nc
+
+  lemma weakening2 : ∀ Γ A, Γ ⊢ A → ∀ Δ, Γ ⊆ Δ → Δ ⊢ A :=
+  λ Γ A H, Nc.induction_on H
+    (λ Γ A Hin Δ Hs,                   !Nax  (Hs A Hin))
+    (λ Γ A B H w Δ Hs,                 !ImpI (w _ (cons_sub_cons A Hs)))
+    (λ Γ A B H₁ H₂ w₁ w₂ Δ Hs,         !ImpE (w₁ _ Hs) (w₂ _ Hs))
+    (λ Γ A H w Δ Hs,                   !BotC (w _ (cons_sub_cons (~A) Hs)))
+    (λ Γ A B H₁ H₂ w₁ w₂ Δ Hs,         !AndI (w₁ _ Hs) (w₂ _ Hs))
+    (λ Γ A B H w Δ Hs,                 !AndE₁ (w _ Hs))
+    (λ Γ A B H w Δ Hs,                 !AndE₂ (w _ Hs))
+    (λ Γ A B H w Δ Hs,                 !OrI₁ (w _ Hs))
+    (λ Γ A B H w Δ Hs,                 !OrI₂ (w _ Hs))
+    (λ Γ A B C H₁ H₂ H₃ w₁ w₂ w₃ Δ Hs, !OrE (w₁ _ Hs) (w₂ _ (cons_sub_cons A Hs)) (w₃ _ (cons_sub_cons B Hs)))
+
+  lemma weakening : ∀ Γ Δ A, Γ ⊢ A → (Γ++Δ) ⊢ A :=
+  λ Γ Δ A H, weakening2 Γ A H (Γ++Δ) (sub_append_left Γ Δ)
+
+  lemma deduction : ∀ Γ A B, Γ ⊢ (A ⇒ B) → (A::Γ) ⊢ B :=
+  λ Γ A B H, ImpE _ A _ (!weakening2 H _ (sub_cons A Γ)) (!Nax (mem_cons A Γ))
+
+  lemma prov_impl : ∀ A B, Provable (A ⇒ B) → ∀ Γ, Γ ⊢ A → Γ ⊢ B :=
+  λ A B Hp Γ Ha,
+    have wHp : Γ ⊢ (A ⇒ B), from !weakening Hp,
+    !ImpE wHp Ha
+
+  lemma Satisfies_cons : ∀ {A Γ v}, Satisfies v Γ → is_true (TrueQ v A) → Satisfies v (A::Γ) :=
+  λ A Γ v s t B BinAG,
+    or.elim BinAG
+      (λ e : B = A, by rewrite e; exact t)
+      (λ i : B ∈ Γ, s _ i)
+
+  theorem Soundness_general : ∀ A Γ, Γ ⊢ A → Γ ⊨ A :=
+  λ A Γ H, Nc.induction_on H
+    (λ Γ A Hin v s,   (s _ Hin))
+    (λ Γ A B H r v s,
+      by_cases
+        (λ t : is_true (TrueQ v A),
+           have aux₁ : Satisfies v (A::Γ), from Satisfies_cons s t,
+           have aux₂ : is_true (TrueQ v B), from r v aux₁,
+           bor_inr aux₂)
+        (λ f : ¬ is_true (TrueQ v A),
+           have aux : bnot (TrueQ v A) = tt, by rewrite (eq_ff_of_ne_tt f),
+           bor_inl aux))
+    (λ Γ A B H₁ H₂ r₁ r₂ v s,
+       assert aux₁ : bnot (TrueQ v A) || TrueQ v B = tt, from r₁ v s,
+       assert aux₂ : TrueQ v A = tt, from r₂ v s,
+       by rewrite [aux₂ at aux₁, bnot_true at aux₁, ff_bor at aux₁]; exact aux₁)
+    (λ Γ A H r v s, by_contradiction
+       (λ n : TrueQ v A ≠ tt,
+         assert aux₁ : TrueQ v A    = ff, from eq_ff_of_ne_tt n,
+         assert aux₂ : TrueQ v (~A) = tt, begin change (bnot (TrueQ v A) || ff = tt), rewrite aux₁ end,
+         have aux₃ : Satisfies v ((~A)::Γ), from Satisfies_cons s aux₂,
+         have aux₄ : TrueQ v ⊥ = tt, from r v aux₃,
+         absurd aux₄ ff_ne_tt))
+    (λ Γ A B H₁ H₂ r₁ r₂ v s,
+      have aux₁ : TrueQ v A = tt, from r₁ v s,
+      have aux₂ : TrueQ v B = tt, from r₂ v s,
+      band_intro aux₁ aux₂)
+    (λ Γ A B H r v s,
+      have aux : TrueQ v (A ∧ B) = tt, from r v s,
+      band_elim_left aux)
+    (λ Γ A B H r v s,
+      have aux : TrueQ v (A ∧ B) = tt, from r v s,
+      band_elim_right aux)
+    (λ Γ A B H r v s,
+      have aux : TrueQ v A = tt, from r v s,
+      bor_inl aux)
+    (λ Γ A B H r v s,
+      have aux : TrueQ v B = tt, from r v s,
+      bor_inr aux)
+    (λ Γ A B C H₁ H₂ H₃ r₁ r₂ r₃ v s,
+      have aux : TrueQ v A || TrueQ v B = tt, from r₁ v s,
+      or.elim (or_of_bor_eq aux)
+        (λ At : TrueQ v A = tt,
+          have aux : Satisfies v (A::Γ), from Satisfies_cons s At,
+          r₂ v aux)
+        (λ Bt : TrueQ v B = tt,
+          have aux : Satisfies v (B::Γ), from Satisfies_cons s Bt,
+          r₃ v aux))
+
+  theorem Soundness : Prop_Soundness :=
+  λ A, Soundness_general A []
+
+end PropF