進捗

lambda.v

Require Import List.
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.EqNat.
Require Import Coq.Lists.ListSet.

Definition nat_eq : forall x y : nat, {x = y} + {x <> y}.
  decide equality.
Defined.

Inductive term : Set :=
  | var : nat -> term
  | app : term -> term -> term
  | abs : nat -> term -> term.

Fixpoint V (t : term) : set nat :=
  match t with
  | var v => set_add nat_eq v (empty_set nat)
  | app m n => set_union nat_eq (V m) (V n)
  | abs v m => set_add nat_eq v (V m)
  end.

Fixpoint FV (t : term) : set nat :=
  match t with
  | var v => set_add nat_eq v (empty_set nat)
  | app m n => set_union nat_eq (V m) (V n)
  | abs v m => set_remove nat_eq v (V m)
  end.


Fixpoint BV (t : term) : set nat :=
  match t with
  | var v => empty_set nat
  | app m n => set_union nat_eq (V m) (V n)
  | abs v m => set_add nat_eq v (V m)
  end.

Fixpoint substitute (x : nat) (n m : term) : term :=
  match m with
  | var y => if beq_nat x y then n else var y
  | app q r => app (substitute x n q) (substitute x n r)
  | abs y q => abs y (substitute x n q)
  end.