hoge2.v

Require Import ssreflect.

Axiom SET : Type.

Definition Var := nat.
Definition Term := nat.


(*
Definition equalS : nat := 0.
Definition memS : nat := 1.
Definition notS : nat := 2.
Definition orS : nat := 3.
Definition andS : nat := 4.
Definition implS : nat := 5.
Definition forallS : Term -> nat :=
  fun t => 6.
Definition existsS : Term -> nat :=
  fun t => 7.
*)

Inductive Fml : Type :=
  | equality : Var -> Var -> Fml
  | membership : Var -> Var -> Fml
  | notS : Fml -> Fml
  | orS : Fml -> Fml -> Fml
  | andS : Fml -> Fml -> Fml
  | implS : Fml -> Fml -> Fml
  | forallS : Var -> Fml -> Fml
  | existsS : Var -> Fml -> Fml.

Notation "x _=_ y" := (equality x y) (at level 50).
Notation "x _∈_ y" := (membership x y) (at level 50).
Notation "￢ x" := (notS x) (at level 51).
Notation "x ∨ y" := (orS x y) (at level 51).
Notation "x ∧ y" := (andS x y) (at level 51).
Notation "x → y" := (implS x y) (at level 51).
Notation "∀ x , y" := (forallS x y) (at level 51).
Notation "∃ x , y" := (existsS x y) (at level 51).

Definition X : Fml := 0 _=_ 0 ∧ 1 _=_ 1.

Definition is_atomic (f : Fml) : Prop :=
  match f with
   | equality x y => True
   | membership x y => True
   | notS f0 => False
   | orS f0 f1 => False
   | andS f0 f1 => False
   | implS f0 f1 => False
   | forallS x f0 => False
   | existsS x f0 => False
end.

Eval compute in (is_atomic (0 _=_ 0)).

Definition is_bounded_qf (f : Fml) : Prop :=
  match f with
   | equality x y => False
   | membership x y => False
   | notS f0 => False
   | orS f0 f1 => False
   | andS f0 f1 => False
   | implS f0 f1 => False
   | forallS x f0 =>
     match f0 with
       | equality z w => False
       | membership z w => False
       | notS f0 => False
       | orS f0 f1 => False
       | andS f0 f1 => False
       | implS f0 f1 =>
         match f0 with
           | equality z w => False
           | membership z w => (z = x)
           | notS f0 => False
           | orS f0 f1 => False
           | andS f0 f1 => False
           | implS f0 f1 => False
           | forallS x f0 => False
           | existsS x f0 => False
         end
       | forallS x f0 => False
       | existsS x f0 => False
     end
   | existsS x f0 =>
     match f0 with
       | equality z w => False
       | membership z w => False
       | notS f0 => False
       | orS f0 f1 => False
       | andS f0 f1 => False
       | implS f0 f1 =>
         match f0 with
           | equality z w => False
           | membership z w => (z = x)
           | notS f0 => False
           | orS f0 f1 => False
           | andS f0 f1 => False
           | implS f0 f1 => False
           | forallS x f0 => False
           | existsS x f0 => False
         end
       | forallS x f0 => False
       | existsS x f0 => False
     end
end.

Eval compute in is_bounded_qf (∀1 , (1 _=_ 0)).
  (* ====> false *)
Eval compute in is_bounded_qf (∀1 , (1 _∈_ 2)).
  (* ====> false *)
Example testcase0: is_bounded_qf (∀1 , ((1 _∈_ 2) → (1 _=_ 3))).
  (* ====> true *)
Proof.
  simpl.
  reflexivity.
Qed.

Definition is_not_qf (f : Fml) : Prop :=
  match f with
   | equality x y => True
   | membership x y => True
   | notS f0 => True
   | orS f0 f1 => True
   | andS f0 f1 => True
   | implS f0 f1 => True
   | forallS x f0 => False
   | existsS x f0 => False
end.

Fixpoint is_quantifier_free (f : Fml) : Prop :=
  match f with
   | equality x y => True
   | membership x y => True
   | notS f0 => (is_quantifier_free f0)
   | orS f0 f1 => (is_quantifier_free f0)/\(is_quantifier_free f1)
   | andS f0 f1 => (is_quantifier_free f0)/\(is_quantifier_free f1)
   | implS f0 f1 => (is_quantifier_free f0)/\(is_quantifier_free f1)
   | forallS x f0 => False
   | existsS x f0 => False
end.

Require Import Datatypes.
Check (sum unit unit).

Definition hoge (a : bool) : (unit + unit) :=
  match a with
  | true => inl tt
  | false => inr tt
  end.


Definition bound_var (f : Fml) : (Var+unit) :=
  match f with
    | equality z w => tt
    | membership z w => tt
    | notS f0 => tt
    | orS f0 f1 => tt
    | andS f0 f1 => tt
    | implS f0 f1 =>
      match f0 with
        | equality z w => tt
        | membership z w => z
        | notS f0 => tt
        | orS f0 f1 => tt
        | andS f0 f1 => tt
        | implS f0 f1 => tt
        | forallS x f0 => tt
        | existsS x f0 => tt
      end
    | forallS x f0 => tt
    | existsS x f0 => tt
  end.

Fixpoint is_Σ_0 (f : Fml) : Prop :=
  match f with
   | equality x y => True
   | membership x y => True
   | notS f0 => (is_Σ_0 f0)
   | orS f0 f1 => (is_Σ_0 f0)/\(is_Σ_0 f1)
   | andS f0 f1 => (is_Σ_0 f0)/\(is_Σ_0 f1)
   | implS f0 f1 => (is_Σ_0 f0)/\(is_Σ_0 f1)
   | forallS x f0 => 
     match f0 with
       |
   | existsS x f0 => False