如何证明 agda 中一种简单语言的弱化？

Question

我正在尝试证明与 PFPL 第 4 章中哈珀的类似的弱化引理。即，weakening : {x : String} {Γ : Context} {e : Expr} {τ τ' : Type} → x ∉dom Γ → Γ ⊢ e ؛ τ' → (Γ , x ؛ τ) ⊢ e ؛ τ'

我改编了 Wadler 的一些代码，他在下面证明了 weaken，但仍然不知道如何证明这个一般的 weakening 引理，要么使用重命名函数，要么通过归纳法正如哈珀所做的那样。（例如，哈珀似乎隐含地假设交换了一个 let 构造函数，不包括在这种语言中）。我认为引入 _∉dom_ 会有所帮助，但我只是看到它膨胀了我必须做的大量工作，以某种方式用 _؛_∈_ 制作一堆对应引理。

如何通过归纳或 rename 证明 weakening，如陈述的或修改的？

module basic where

open import Data.List using (List; _∷_; []; map)
open import Data.Empty
open import Data.String using (_++_; _==_; _≟_; String)
open import Data.Nat using (ℕ)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)

data Type : Set where
  nat : Type
  bool : Type

data Expr : Set where
  var : String → Expr
  lit : (n : ℕ) → Expr
  tt : Expr
  ff : Expr
  _+'_ : Expr → Expr → Expr
  _*'_ : Expr → Expr → Expr
  _<'_ : Expr → Expr → Expr
  if : Expr → Expr → Expr → Expr

Id : Set
Id = String

infixl 5  _,_؛_
data Context : Set where
  ∅     : Context
  _,_؛_ : Context → Id → Type → Context


data _؛_∈_ : Id → Type → Context → Set where
  Z : ∀ {Γ x A} → x ؛ A ∈ (Γ , x ؛ A)
  S : ∀ {Γ x y A B} → (x ≡ y → ⊥) → x ؛ A ∈ Γ → x ؛ A ∈ (Γ , y ؛ B)

-- not in wadler
data _∉dom_ : Id → Context → Set where
  em :  ∀ {x} → x ∉dom ∅
  notcons  : ∀ {x y τ Γ} → x ∉dom Γ → (x ≡ y → ⊥) → x ∉dom (Γ , y ؛ τ )

-- hypothetical judgement
data _⊢_؛_ : Context → Expr → Type → Set where 
  varR   : ∀ {a τ Γ} → (a ؛ τ ∈ Γ) → (Γ ⊢ (var a) ؛ τ)
  natR : ∀ {Γ} {n : ℕ}  → Γ ⊢ (lit n) ؛ nat
  trueR :  ∀ {Γ} → Γ ⊢ tt ؛ bool
  falseR :  ∀ {Γ} → Γ ⊢ ff ؛ bool
  plus-i :  ∀ {Γ} {e1 e2 : Expr} → Γ ⊢ e1 ؛ nat → Γ ⊢ e2 ؛ nat → Γ ⊢ e1 +' e2 ؛ nat
  times-i :  ∀ {Γ} {e1 e2 : Expr} → Γ ⊢ e1 ؛ nat → Γ ⊢ e2 ؛ nat → Γ ⊢ e1 *' e2 ؛ nat
  le-i :  ∀ {Γ} {e1 e2 : Expr} → Γ ⊢ e1 ؛ nat → Γ ⊢ e2 ؛ nat → Γ ⊢ e1 <' e2 ؛ bool
  if-i :  ∀ {Γ} {τ} {e1 e2 e3 : Expr}  → Γ ⊢ e1 ؛ bool → Γ ⊢ e2 ؛ τ → Γ ⊢ e3 ؛ τ → Γ ⊢ if e1 e2 e3 ؛ τ 

-- adapted from wadler
rename : ∀ {Γ Δ} → (∀ {x A} → x ؛ A ∈ Γ → x ؛ A ∈ Δ) → (∀ {M A} → Γ ⊢ M ؛ A → Δ ⊢ M ؛ A)
rename f (varR x) = varR (f x)
rename f natR = natR
rename f trueR = trueR
rename f falseR = falseR
rename f (plus-i h h₁) = plus-i (rename f h) (rename f h₁)
rename f (times-i h h₁) = times-i (rename f h) (rename f h₁)
rename f (le-i h h₁) = le-i (rename f h) (rename f h₁)
rename f (if-i h h₁ h₂) = if-i (rename f h) (rename f h₁) (rename f h₂)

-- wadler's weaken lemma
weaken : ∀ {Γ M A} → ∅ ⊢ M ؛ A → Γ ⊢ M ؛ A
weaken x = rename (λ ()) x

-- my attempt
weakening : {x : String} {Γ : Context} {e : Expr} {τ τ' : Type} → x ∉dom Γ → Γ ⊢ e ؛ τ' → (Γ , x ؛ τ)  ⊢ e ؛ τ' 
-- induction, dunno how to account for the variable
weakening x (varR y) = {!!}
weakening x natR = natR
weakening x trueR = trueR
weakening x falseR = falseR
weakening x (plus-i y₁ y₂) = plus-i (weakening x y₁) (weakening x y₂)
weakening x (times-i y₁ y₂) = times-i (weakening x y₁) (weakening x y₂)
weakening x (le-i y₁ y₂) = le-i (weakening x y₁) (weakening x y₂)
weakening x (if-i y₁ y₂ y₃) = if-i (weakening x y₁) (weakening x y₂) (weakening x y₃)

-- otherwise, i don't know how to addapt this rename
weakening' : {x : String} {Γ : Context} {e : Expr} {τ τ' : Type} → x ∉dom Γ → Γ ⊢ e ؛ τ' → (Γ , x ؛ τ)  ⊢ e ؛ τ' 
weakening' {x} {τ = τ} em y = rename help y
  where
    help : {x = x₁ : Id} {A : Type} → x₁ ؛ A ∈ ∅ → x₁ ؛ A ∈ (∅ , x ؛ τ)
    help {x = x₁} ()
weakening' (notcons α β) y = rename (λ z → S (λ x₃ → {!!}) z) y

Answer 1

一个可能的想法是添加一个引理，该引理指出，如果值 x 不在上下文 Γ 中并且值 a 的类型为 τ 在相同的上下文中 Γ 那么 a 和 x 不能相等。

open import Relation.Nullary

-- If a,τ'∈Γ and x∉Γ then ¬a≡x
prop : ∀ {x Γ τ a} → x ∉dom Γ → a ؛ τ ∈ Γ → ¬ a ≡ x
prop (notcons _ ¬x≡x) Z refl = ¬x≡x refl
prop (notcons x∉Γ _) (S _ aτ∈Γ) = prop x∉Γ aτ∈Γ

那么你的weaking simple版本中缺失的case就变成了

weakening x (varR y) = varR (S (prop x y) y)

如何证明 agda 中一种简单语言的弱化？

How does one prove weakening for a simple language in agda?

language-design

agda

theorem-proving

induction