(* File: Weight.v  (last edited on 27/10/2000) (c) Klaus Weich  *)


Require Import Rules.


Fixpoint weight (a : form) : nat :=
  match a with
  | Falsum => 1
  | Atom _ => 1
  | AndF a b => S (weight a + weight b)
  | OrF Falsum b => S (weight b)
  | OrF (Atom _) b => S (weight b)
  | OrF a b => S (S (weight b + weight a))
  | Imp a b => weight_neg a + weight b
  end
 
 with weight_neg (a : form) : nat :=
  match a with
  | Falsum => 0
  | Atom _ => 0
  | AndF a b => S (weight_neg a + weight_neg b)
  | OrF a b => S (S (S (weight_neg a + weight_neg b)))
  | Imp Falsum b => 1
  | Imp (Atom _) Falsum => 2
  | Imp (Atom _) (Atom _) => 1
  | Imp (Atom _) b => S (S (S (weight_neg b)))
  | Imp a b => S (S (S (S (weight_neg b + weight a))))
  end.


Fixpoint weight_goal (a : form) : nat :=
  match a with
  | Falsum => 0
  | Atom _ => 0
  | AndF _ _ => 1
  | OrF _ _ => 1
  | Imp _ b => S (weight_goal b)
  end.


Definition weight_gamma :=
  fold_right (fun (a : form) (n : nat) => weight a + n) 0.

(**********************************************************************)

Lemma weight_ge_1 : forall a : form, 1 <= weight a.
(* Goal: forall a : form, le (S O) (weight a) *)
intros a; elim a; clear a.
(* Goal: forall i : Int, le (S O) (weight (Atom i)) *)
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (AndF f f0)) *)
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (OrF f f0)) *)
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (Imp f f0)) *)
trivial.
(* Goal: forall i : Int, le (S O) (weight (Atom i)) *)
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (AndF f f0)) *)
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (OrF f f0)) *)
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (Imp f f0)) *)
trivial.
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (AndF f f0)) *)
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (OrF f f0)) *)
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (Imp f f0)) *)
intros; simpl in |- *.
(* Goal: le (S O) (S (Nat.add (weight f) (weight f0))) *)
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (OrF f f0)) *)
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (Imp f f0)) *)
apply le_n_S.
(* Goal: le O (weight_neg a) *)
apply le_O_n.
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (Imp f f0)) *)
intros a ih_a b ih_b.
(* Goal: le (S O) (weight (OrF a b)) *)
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (Imp f f0)) *)
clear ih_a ih_b.
(* Goal: le O (weight_neg a) *)
case a; clear a; intros; simpl in |- *; apply le_n_S; apply le_O_n.
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (Imp f f0)) *)
intros a ih_a b ih_b.
(* Goal: le (S (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma))) (weight_gamma (@cons form d gamma)) *)
simpl in |- *.
(* Goal: le (S O) (Nat.add (weight_neg a) (weight b)) *)
fold weight_neg in |- *.
(* Goal: le (S O) (Nat.add (weight_neg a) (weight b)) *)
apply le_trans with (weight b); try assumption.
(* Goal: le (weight b) (Nat.add (weight_neg a) (weight b)) *)
apply (plus_le_compat_r 0 (weight_neg a) (weight b)).
(* Goal: le O (weight_neg a) *)
apply le_O_n.
Qed.

Lemma weight_neg_le :
 forall (j : Int) (a : form),
 weight_neg (Imp (Atom j) a) <= S (S (S (weight_neg a))).
(* Goal: forall (j : Int) (a : form), le (weight_neg (Imp (Atom j) a)) (S (S (S (weight_neg a)))) *)
intros j a; case a; clear a.
(* Goal: le (weight_neg (Imp (Atom j) Falsum)) (S (S (S (weight_neg Falsum)))) *)
(* Goal: forall i : Int, le (weight_neg (Imp (Atom j) (Atom i))) (S (S (S (weight_neg (Atom i))))) *)
(* Goal: forall f f0 : form, le (weight_neg (Imp (Atom j) (AndF f f0))) (S (S (S (weight_neg (AndF f f0))))) *)
(* Goal: forall f f0 : form, le (weight_neg (Imp (Atom j) (OrF f f0))) (S (S (S (weight_neg (OrF f f0))))) *)
(* Goal: forall f f0 : form, le (weight_neg (Imp (Atom j) (Imp f f0))) (S (S (S (weight_neg (Imp f f0))))) *)
apply le_n_Sn.
(* Goal: le (weight_neg (Imp (Atom j) Falsum)) (S (S (S (weight_neg Falsum)))) *)
(* Goal: forall i : Int, le (weight_neg (Imp (Atom j) (Atom i))) (S (S (S (weight_neg (Atom i))))) *)
(* Goal: forall f f0 : form, le (weight_neg (Imp (Atom j) (AndF f f0))) (S (S (S (weight_neg (AndF f f0))))) *)
(* Goal: forall f f0 : form, le (weight_neg (Imp (Atom j) (OrF f f0))) (S (S (S (weight_neg (OrF f f0))))) *)
(* Goal: forall f f0 : form, le (weight_neg (Imp (Atom j) (Imp f f0))) (S (S (S (weight_neg (Imp f f0))))) *)
intros; apply le_trans with 2; apply le_n_Sn.
(* Goal: forall f f0 : form, le (weight_neg (Imp (Atom j) (Imp f f0))) (S (S (S (weight_neg (Imp f f0))))) *)
intros; apply le_n.
(* Goal: forall f f0 : form, le (weight_neg (Imp (Atom j) (Imp f f0))) (S (S (S (weight_neg (Imp f f0))))) *)
intros; apply le_n.
(* Goal: forall f f0 : form, le (weight_neg (Imp (Atom j) (Imp f f0))) (S (S (S (weight_neg (Imp f f0))))) *)
intros; apply le_n.
Qed.


Lemma weight_vimp :
 forall (l : list Int) (a : form), weight (vimp l a) = weight a.
(* Goal: forall (l : list Int) (a : form), @eq nat (weight (vimp l a)) (weight a) *)
intros l.
(* Goal: forall a : form, @eq nat (weight (vimp l a)) (weight a) *)
elim l; clear l.
(* Goal: forall i : Int, le (S O) (weight (Atom i)) *)
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (AndF f f0)) *)
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (OrF f f0)) *)
(* Goal: forall (f : form) (_ : le (S O) (weight f)) (f0 : form) (_ : le (S O) (weight f0)), le (S O) (weight (Imp f f0)) *)
intro a; trivial.
(* Goal: forall (a : Int) (l : list Int) (_ : forall a0 : form, @eq nat (weight (vimp l a0)) (weight a0)) (a0 : form), @eq nat (weight (vimp (@cons Int a l) a0)) (weight a0) *)
intros i l ih a.
(* Goal: le (S (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma))) (weight_gamma (@cons form d gamma)) *)
simpl in |- *.
(* Goal: @eq nat (weight (vimp l (Imp (Atom i) a))) (weight a) *)
apply ih with (a := Imp (Atom i) a).
Qed.



Lemma weight_gamma_weak :
 forall (a b : form) (gamma : flist) (n : nat),
 weight a < weight b ->
 weight_gamma (b :: gamma) < S n -> weight_gamma (a :: gamma) < n.
(* Goal: forall (a b c d : form) (gamma : flist) (n : nat) (_ : lt (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight d)) (_ : lt (Nat.add (weight d) (weight_gamma gamma)) (S n)), lt (Nat.add (weight a) (Nat.add (weight b) (Nat.add (weight c) (weight_gamma gamma)))) n *)
intros.
(* Goal: le (S (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma))) (weight_gamma (@cons form d gamma)) *)
simpl in |- *.
(* Goal: lt (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma)) n *)
apply lt_S_n.
(* Goal: lt (S (Nat.add (weight a) (weight_gamma gamma))) (S n) *)
apply le_lt_trans with (weight_gamma (b :: gamma)); try assumption.
(* Goal: le (S (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma))) (weight_gamma (@cons form d gamma)) *)
simpl in |- *.
(* Goal: le (S (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma))) (Nat.add (weight d) (weight_gamma gamma)) *)
apply lt_le_S.
(* Goal: lt (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma)) (Nat.add (weight d) (weight_gamma gamma)) *)
apply plus_lt_compat_r.
(* Goal: lt (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight d) *)
assumption.
Qed.


Lemma weight_gamma_weak' :
 forall (a b : form) (gamma : flist) (n : nat),
 weight a < weight b ->
 weight b + weight_gamma gamma < S n -> weight a + weight_gamma gamma < n.
(* Goal: forall (a b c d : form) (gamma : flist) (n : nat) (_ : lt (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight d)) (_ : lt (Nat.add (weight d) (weight_gamma gamma)) (S n)), lt (Nat.add (weight a) (Nat.add (weight b) (Nat.add (weight c) (weight_gamma gamma)))) n *)
intros.
(* Goal: lt (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight d) *)
apply (weight_gamma_weak a b gamma n); assumption.
Qed.


Lemma weight_gamma_weak2 :
 forall (a b c : form) (gamma : flist) (n : nat),
 weight a + weight b < weight c ->
 weight_gamma (c :: gamma) < S n -> weight_gamma (a :: b :: gamma) < n.
(* Goal: forall (a b c d : form) (gamma : flist) (n : nat) (_ : lt (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight d)) (_ : lt (Nat.add (weight d) (weight_gamma gamma)) (S n)), lt (Nat.add (weight a) (Nat.add (weight b) (Nat.add (weight c) (weight_gamma gamma)))) n *)
intros.
(* Goal: le (S (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma))) (weight_gamma (@cons form d gamma)) *)
simpl in |- *.
(* Goal: lt (Nat.add (Nat.add (weight a) (weight b)) (Nat.add (weight c) (weight_gamma gamma))) n *)
apply lt_plus_assoc_l.
(* Goal: lt (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma)) n *)
apply lt_S_n.
(* Goal: lt (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight d) *)
apply le_lt_trans with (weight_gamma (c :: gamma)); try assumption.
(* Goal: le (S (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma))) (weight_gamma (@cons form d gamma)) *)
simpl in |- *.
(* Goal: le (S (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma))) (Nat.add (weight d) (weight_gamma gamma)) *)
apply lt_le_S.
(* Goal: lt (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma)) (Nat.add (weight d) (weight_gamma gamma)) *)
apply plus_lt_compat_r.
(* Goal: lt (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight d) *)
assumption.
Qed.


Lemma weight_gamma_weak2' :
 forall (a b c : form) (gamma : flist) (n : nat),
 weight a + weight b < weight c ->
 weight c + weight_gamma gamma < S n ->
 weight a + (weight b + weight_gamma gamma) < n.
(* Goal: forall (a b c d : form) (gamma : flist) (n : nat) (_ : lt (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight d)) (_ : lt (Nat.add (weight d) (weight_gamma gamma)) (S n)), lt (Nat.add (weight a) (Nat.add (weight b) (Nat.add (weight c) (weight_gamma gamma)))) n *)
intros.
(* Goal: lt (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight d) *)
apply (weight_gamma_weak2 a b c gamma n); assumption.
Qed.


Lemma weight_gamma_weak3 :
 forall (a b c d : form) (gamma : flist) (n : nat),
 weight a + weight b + weight c < weight d ->
 weight_gamma (d :: gamma) < S n -> weight_gamma (a :: b :: c :: gamma) < n.
(* Goal: forall (a b c d : form) (gamma : flist) (n : nat) (_ : lt (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight d)) (_ : lt (Nat.add (weight d) (weight_gamma gamma)) (S n)), lt (Nat.add (weight a) (Nat.add (weight b) (Nat.add (weight c) (weight_gamma gamma)))) n *)
intros.
(* Goal: le (S (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma))) (weight_gamma (@cons form d gamma)) *)
simpl in |- *.
(* Goal: lt (Nat.add (Nat.add (weight a) (weight b)) (Nat.add (weight c) (weight_gamma gamma))) n *)
apply lt_plus_assoc_l.
(* Goal: lt (Nat.add (Nat.add (weight a) (weight b)) (Nat.add (weight c) (weight_gamma gamma))) n *)
apply lt_plus_assoc_l.
(* Goal: lt (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma)) n *)
apply lt_S_n.
(* Goal: lt (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight d) *)
apply le_lt_trans with (weight_gamma (d :: gamma)); try assumption.
(* Goal: le (S (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma))) (weight_gamma (@cons form d gamma)) *)
simpl in |- *.
(* Goal: le (S (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma))) (Nat.add (weight d) (weight_gamma gamma)) *)
apply lt_le_S.
(* Goal: lt (Nat.add (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight_gamma gamma)) (Nat.add (weight d) (weight_gamma gamma)) *)
apply plus_lt_compat_r.
(* Goal: lt (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight d) *)
assumption.
Qed.


Lemma weight_gamma_weak3' :
 forall (a b c d : form) (gamma : flist) (n : nat),
 weight a + weight b + weight c < weight d ->
 weight d + weight_gamma gamma < S n ->
 weight a + (weight b + (weight c + weight_gamma gamma)) < n.
(* Goal: forall (a b c d : form) (gamma : flist) (n : nat) (_ : lt (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight d)) (_ : lt (Nat.add (weight d) (weight_gamma gamma)) (S n)), lt (Nat.add (weight a) (Nat.add (weight b) (Nat.add (weight c) (weight_gamma gamma)))) n *)
intros.
(* Goal: lt (Nat.add (Nat.add (weight a) (weight b)) (weight c)) (weight d) *)
apply (weight_gamma_weak3 a b c d gamma n); assumption.
Qed.
