coq prop formulas

(*Basé sur le travail de P. Dehornoy, DehornoyChap6.pdf*)

Require Import Arith.
Require Import List.

(*Variables propositionnelles*)

(*Formules*)
Inductive PFormule :=
| FVar : nat -> PFormule
| FNeg : PFormule -> PFormule
| FAnd : PFormule -> PFormule -> PFormule
| FOr : PFormule -> PFormule -> PFormule
| FImply : PFormule -> PFormule -> PFormule.

Theorem PFormule_eq_dec : forall (p q : PFormule), {p=q}+{p<>q}.
	repeat (decide equality).
Qed.

Delimit Scope PFormule_scope with prop.
Bind Scope PFormule_scope with PFormule.
Local Open Scope PFormule_scope.

Notation "'X' i" := (FVar i) (at level 5).
Notation "~ F" := (FNeg F).
Notation "F /\ G" := (FAnd F G).
Notation "F \/ G" := (FOr F G).
Notation "F -> G" := (FImply F G) : PFormule_scope.
Notation "F <-> G" := (FAnd (FImply F G) (FImply G F)).


Definition X1 := X 1.
Definition X2 := X 2.
Definition X3 := X 3.

(*Implication*)
Definition A1:PFormule := X1 -> X2 -> X1.
Definition A2:PFormule := (X1->(X2->X3))->((X1->X2)->(X1->X3)).

(*Négation*)
Definition A3:PFormule := X1-> ~~X1.
Definition A4:PFormule := ~~X1->X1.
Definition A5:PFormule:= (X1->X2)->(~X2->~X1).

(*Conjonction*)
Definition A6:PFormule := X1->(X2->(X1/\X2)).
Definition A7:PFormule := (X1/\X2)->X1.
Definition A8:PFormule := (X1/\X2)->X2.

(*Disjonction*)
Definition A9:PFormule  := X1->(X1\/X2).
Definition A10:PFormule := X2->(X1\/X2).
Definition A11:PFormule := ~X1->((X1\/X2)->X2).

Inductive AProp : PFormule -> Prop :=
| a1: AProp A1
| a2 : AProp A2
| a3 : AProp A3
| a4 : AProp A4
| a5 : AProp A5
| a6 : AProp A6
| a7 : AProp A7
| a8 : AProp A8
| a9 : AProp A9
| a10 : AProp A10
| a11 : AProp A11.


(*Variables libres et substitutions*)
(*Basé sur le travail de Gyesik Lee "Proof Pearl : substitution revisited, again"*)
Fixpoint FV (F : PFormule) : list nat :=
match F with
| FVar x => x :: nil
| FNeg F => FV F
| FAnd F G | FOr F G | FImply F G => (FV F) ++ (FV G)
end.

Definition substitution := (nat -> PFormule)%type.

(** Mise à jour d'une fonction avec une nouvelle valeur*)
Definition up (f : nat -> PFormule) (e : PFormule) (d : nat) : nat -> PFormule :=
fun x => if eq_nat_dec x d then e else f x.
Notation " f [[ e => d ]] " := (up f e d) (at level 70).

Fixpoint subst (F : PFormule) (rho : substitution) {struct F} : PFormule :=
  match F with
    | FVar n     => rho n
    | FNeg F     => FNeg (subst F rho)
    | FAnd F1 F2 => FAnd (subst F1 rho) (subst F2 rho)
    | FOr F1 F2  => FOr (subst F1 rho) (subst F2 rho)
    | FImply F1 F2 => FImply (subst F1 rho) (subst F2 rho)
    end.

Notation id := (fun (n : nat) => FVar n).

Notation " M {{ rho }} " := (subst M rho) (at level 55).

(*Demonstration*)
Inductive Pdemonstration :=
|PdemonstrationInst : forall F l, (exists A s, (AProp A /\ (subst A s) = F)%type)-> Pdemonstration  F (F::l)
|PdemonstrationCoupure : forall F G l, In F l -> In (F->G) l -> Pdemonstration G (G::l).


Definition verification (l : list PFormule) (f : PFormule) : option {d:Pdemonstration | Pdemonstration f l}.

Local Close Scope PFormule_scope.