ND.v

(* 자연연역의 monotonicity 성질을 coq으로 형식증명하다가 질문이 생겼습니다. *)

(* 먼저 저는 자연연역을 다음과 같이 정의했습니다. *)
Inductive infers {L: language} (Gamma: ensemble (@frm L)) : forall C: (@frm L), Prop :=
| By_hyp p
  (IN: p \in Gamma) (* p가 Gamma의 원소일 때 *)
  : Gamma ⊢ p       (* Gamma ⊢ p이다 *)
| (* ... *)
| Forall_intro x y p1
  (NOT_FREE1: is_not_free_in_frms y Gamma)                   (* y가 Gamma에 자유롭게 나타나는 개체변수가 아니고)
  (NOT_FREE2: is_not_free_in_frm y (All_frm x p1))           (* y가 (∀x)p1에 자유롭게 나타나지 않으며 *)
  (INFERS1: Gamma ⊢ subst_frm (one_subst x (IVar_trm y)) p1) (* Gamma ⊢ [y/x]p1이면 *)
  : Gamma ⊢ All_frm x p1                                     (* Gamma ⊢ (∀x)p1이다. *)
| (* ... *)
where " Gamma ⊢ C " := (infers Gamma C).

(* 이제 the monotonicity property of natural deduction을 증명하다가 문제가 생겼습니다. *)
Lemma extend_infers {L: language} (Gamma: ensemble (@frm L)) (Delta: ensemble (@frm L)) (C: @frm L)
  (SUBSET: Gamma \subseteq Delta)
  (INFERS: Gamma ⊢ C)
  : Delta ⊢ C.
(* 왜냐하면 INFERS에 대해서 귀납법을 적용할 때 *)
(* NOT_FREE1 조건을 해결할 수 없기 때문입니다. *)
(* 즉, Gamma ⊆ Delta이므로 y가 Gamma에 자유롭게 나타나지 않다는 사실로부터 *)
(* Delta에도 자유롭게 나타나지 않는다는 사실을 얻을 수 없기 때문에 생기는 문제입니다. *)
(* 따라서 잘못된 정의라고 생각하게 되었고 어떻게 고치면 될지 조언을 구합니다. *)

NewND.v

#[local] Infix " \in " := E.In.
#[local] Infix " \subseteq " := E.isSubsetOf.
#[local] Notation In := List.In.

Section NATURAL_DEDUCTION.

Import ListNotations.

Context {L: language} (eigenvariable := nat).

Let L' : language := augmented_language L eigenvariable.

Let mkEigenVariable (c: eigenvariable) : trm L' :=
  @Cnst_trm (augmented_language L eigenvariable) (inr c).

Inductive infers {cs: list eigenvariable} (Gamma: ensemble (frm L')) : forall C: (frm L'), Prop :=
| By_hyp p
  (IN: p \in Gamma)
  : Gamma ⊢ p
| Eqn_I t1
  : Gamma ⊢ Eqn_frm t1 t1
| Eqn_E x t1 t2 p1
  (INFERS1: Gamma ⊢ Eqn_frm t1 t2)
  (INFERS2: Gamma ⊢ subst_frm (one_subst x t1) p1)
  : Gamma ⊢ subst_frm (one_subst x t2) p1
| All_I x c p1
  (NOT_IN: ~ In c cs)
  (INFERS1: infers (cs := c :: cs) Gamma (subst_frm (one_subst x (mkEigenVariable c)) p1))
  : Gamma ⊢ All_frm x p1
| All_E x t p
  (INFERS1: Gamma ⊢ All_frm x p)
  : Gamma ⊢ subst_frm (one_subst x t) p
| Exs_I x t p
  (INFERS1: Gamma ⊢ subst_frm (one_subst x t) p)
  : Gamma ⊢ Exs_frm x p
| Exs_E x c p1 p2
  (NOT_IN: ~ In c cs)
  (INFERS1: Gamma ⊢ Exs_frm x p1)
  (INFERS2: infers (cs := c :: cs) (insert (subst_frm (one_subst x (mkEigenVariable c)) p1) Gamma) p2)
  : Gamma ⊢ p2
| Bot_I p1
  (INFERS1: Gamma ⊢ p1)
  (INFERS2: Gamma ⊢ Neg_frm p1)
  : Gamma ⊢ Bot_frm
| Bot_E p1
  (INFERS1: Gamma ⊢ Bot_frm)
  : Gamma ⊢ p1
| Neg_I p1
  (INFERS1: insert p1 Gamma ⊢ Bot_frm)
  : Gamma ⊢ Neg_frm p1
| Neg_E p1
  (INFERS1: insert (Neg_frm p1) Gamma ⊢ Bot_frm)
  : Gamma ⊢ p1
| Con_I p1 p2
  (INFERS1: Gamma ⊢ p1)
  (INFERS2: Gamma ⊢ p2)
  : Gamma ⊢ Con_frm p1 p2
| Con_E1 p1 p2
  (INFERS1: Gamma ⊢ Con_frm p1 p2)
  : Gamma ⊢ p1
| Con_E2 p1 p2
  (INFERS1: Gamma ⊢ Con_frm p1 p2)
  : Gamma ⊢ p2
| Dis_I1 p1 p2
  (INFERS1: Gamma ⊢ p1)
  : Gamma ⊢ Dis_frm p1 p2
| Dis_I2 p1 p2
  (INFERS1: Gamma ⊢ p2)
  : Gamma ⊢ Dis_frm p1 p2
| Dis_E p1 p2 p3
  (INFERS1: Gamma ⊢ Dis_frm p1 p2)
  (INFERS2: insert p1 Gamma ⊢ p3)
  (INFERS3: insert p2 Gamma ⊢ p3)
  : Gamma ⊢ p3
| Imp_I p1 p2
  (INFERS1: insert p1 Gamma ⊢ p2)
  : Gamma ⊢ Imp_frm p1 p2
| Imp_E p1 p2
  (INFERS1: Gamma ⊢ Imp_frm p1 p2)
  (INFERS2: Gamma ⊢ p1)
  : Gamma ⊢ p2
| Iff_I p1 p2
  (INFERS1: insert p1 Gamma ⊢ p2)
  (INFERS2: insert p2 Gamma ⊢ p1)
  : Gamma ⊢ Iff_frm p1 p2
| Iff_E1 p1 p2
  (INFERS1: Gamma ⊢ Iff_frm p1 p2)
  (INFERS2: Gamma ⊢ p1)
  : Gamma ⊢ p2
| Iff_E2 p1 p2
  (INFERS1: Gamma ⊢ Iff_frm p1 p2)
  (INFERS2: Gamma ⊢ p2)
  : Gamma ⊢ p1
where " Gamma ⊢ C " := (infers Gamma C) : type_scope.