(*********************************************************************************************************************************)
-(* NaturalDeduction: structurally explicit proofs in Coq *)
+(* NaturalDeduction: *)
+(* *)
+(* Structurally explicit natural deduction proofs. *)
+(* *)
(*********************************************************************************************************************************)
Generalizable All Variables.
| T_Branch a b => nd_prod (nd_id a) (nd_id b)
end.
+ Fixpoint nd_weak' (sl:Tree ??Judgment) : sl /⋯⋯/ [] :=
+ match sl as SL return SL /⋯⋯/ [] with
+ | T_Leaf None => nd_id0
+ | T_Leaf (Some x) => nd_weak x
+ | T_Branch a b => nd_prod (nd_weak' a) (nd_weak' b) ;; nd_cancelr
+ end.
+
Hint Constructors Structural.
Lemma nd_id_structural : forall sl, Structural (nd_id sl).
intros.
destruct a; auto.
Defined.
+ Lemma weak'_structural : forall a, Structural (nd_weak' a).
+ intros.
+ induction a.
+ destruct a; auto.
+ simpl.
+ auto.
+ simpl.
+ auto.
+ Qed.
+
(* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to
* structural variations *)
Class ND_Relation :=
(* any two _structural_ proofs with the same hypotheses/conclusions must be considered equal *)
; ndr_structural_indistinguishable : forall `(f:a/⋯⋯/b)(g:a/⋯⋯/b), Structural f -> Structural g -> f===g
+
+ (* any two proofs of nothing are "equally good" *)
+ ; ndr_void_proofs_irrelevant : forall `(f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g
}.
(*
apply q2. subst. apply cnd0.
Defined.
+ (* undo the above *)
+ Fixpoint closedNDtoNormalND {c}(cnd:ClosedND c) : ND [] c :=
+ match cnd in ClosedND C return ND [] C with
+ | cnd_weak => nd_id0
+ | cnd_rule h c cndh rhc => closedNDtoNormalND cndh ;; nd_rule rhc
+ | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2)
+ end.
+
Close Scope nd_scope.
Open Scope pf_scope.