1e6b3614ab
@Kha, we now support variable/constant shadowing in patterns.
A constant may occur in a pattern if it is a constructor or tagged with
the new [pattern] attribute. In the standard library, I have tagged
'add', 'zero', 'one', 'bit0', 'bit1' and 'rfl' with this new attribute.
BTW, arbitrary constants and variables may occur nested in type ascriptions and
inaccessible terms.
Here is an example:
meta_definition tactic_result_to_string {A : Type} : tactic_result A → string
| (success a s) := to_string a
| (exception ⌞A⌟ e s) := "Exception: " ++ to_string (e ())
I had to use the inaccessible ⌞A⌟ in the example above, otherwise, we would be shadowing the parameter
{A : Type}, and we would get a type error.
The new validation is performed at to_pattern_fn (parser.cpp).
78 lines
3.1 KiB
Text
78 lines
3.1 KiB
Text
/-
|
||
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.
|
||
|
||
Similar to soundness.lean, but defines Nc in Type.
|
||
The idea is to be able to prove soundness using recursive equations.
|
||
-/
|
||
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
|
||
local notation A ∨ B := Disj A B
|
||
local notation A ∧ B := Conj A B
|
||
infixr `⇒`:27 := Impl
|
||
notation `⊥` := Bot
|
||
|
||
definition Neg A := A ⇒ ⊥
|
||
notation ~ A := Neg A
|
||
definition Top := ~⊥
|
||
notation `⊤` := Top
|
||
definition BiImpl A B := A ⇒ B ∧ B ⇒ A
|
||
infixr `⇔`:27 := BiImpl
|
||
|
||
definition valuation := PropVar → bool
|
||
|
||
reserve infix ` ⊢ `:26
|
||
|
||
/- Provability -/
|
||
|
||
inductive Nc : list PropF → PropF → Type :=
|
||
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
|
||
open Nc
|
||
|
||
-- Remark ⌞t⌟ indicates we should not pattern match on t.
|
||
-- In the following lemma, we only need to pattern match on Γ ⊢ A,
|
||
|
||
lemma weakening2 : ∀ {Γ A Δ}, Γ ⊢ A → Γ ⊆ Δ → Δ ⊢ A
|
||
| Γ A Δ (Nax Γ A Hin) Hs := Nax _ _ (Hs A Hin)
|
||
| Γ (A ⇒ B) Δ (ImpI Γ A B H) Hs := ImpI _ _ _ (weakening2 H (cons_sub_cons A Hs))
|
||
| Γ B Δ (ImpE Γ A B H₁ H₂) Hs := ImpE _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ Hs)
|
||
| Γ A Δ (BotC Γ A H) Hs := BotC _ _ (weakening2 H (cons_sub_cons (~A) Hs))
|
||
| Γ (A ∧ B) Δ (AndI Γ A B H₁ H₂) Hs := AndI _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ Hs)
|
||
| Γ A Δ (AndE₁ Γ A B H) Hs := AndE₁ _ _ _ (weakening2 H Hs)
|
||
| Γ B Δ (AndE₂ Γ A B H) Hs := AndE₂ _ _ _ (weakening2 H Hs)
|
||
| Γ (A ∧ B) Δ (OrI₁ Γ A B H) Hs := OrI₁ _ _ _ (weakening2 H Hs)
|
||
| Γ (A ∨ B) Δ (OrI₂ Γ A B H) Hs := OrI₂ _ _ _ (weakening2 H Hs)
|
||
| Γ C Δ (OrE Γ A B C H₁ H₂ H₃) Hs :=
|
||
OrE _ _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ (cons_sub_cons A Hs)) (weakening2 H₃ (cons_sub_cons B Hs))
|
||
|
||
end PropF
|