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

Require Export In_NGamma.


Definition a_ai_disj (a : atoms) (ai : atomic_imps) :=
  forall i : Int,
  LOOKUP unit i a tt -> forall bs : nf_list, LOOKUP nf_list i ai bs -> False.


Definition a_goal_disj (a : atoms) (goal : Int) :=
  LOOKUP unit goal a tt -> False.






Lemma disjs_insert_ai :
 forall (i : Int) (b : normal_form) (a : atoms) (ai ai' : atomic_imps),
 a_ai_disj a ai ->
 (forall d : unit, ~ LOOKUP unit i a d) ->
 EQUIV_INS nf_list i (cons b) nf_nil ai ai' -> a_ai_disj a ai'.
(* Goal: forall (i : Int) (b : normal_form) (a : atoms) (ai ai' : atomic_imps) (_ : a_ai_disj a ai) (_ : forall d : unit, not (LOOKUP unit i a d)) (_ : EQUIV_INS nf_list i (@cons normal_form b) nf_nil ai ai'), a_ai_disj a ai' *)
intros i b a ai ai'.
(* Goal: forall (_ : a_ai_disj a ai) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a') (_ : forall bs : nf_list, not (LOOKUP nf_list i ai bs)), a_ai_disj a' ai *)
elim a; clear a; intros a avl_a.
(* Goal: forall (_ : a_ai_disj (AVL_intro unit a avl_a) ai) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) (AVL_intro unit a' avl_a')) (_ : forall bs : nf_list, not (LOOKUP nf_list i ai bs)), a_ai_disj (AVL_intro unit a' avl_a') ai *)
elim ai; clear ai; intros ai avl_ai.
(* Goal: forall (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) (AVL_intro unit a' avl_a')) (_ : EQUIV_DEL nf_list i (AVL_intro nf_list ai avl_ai) ai'), a_ai_disj (AVL_intro unit a' avl_a') ai' *)
elim ai'; clear ai'; intros ai' avl_ai'.
(* Goal: forall (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) (AVL_intro unit a' avl_a')) (_ : forall bs : nf_list, not (LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs)), a_ai_disj (AVL_intro unit a' avl_a') (AVL_intro nf_list ai avl_ai) *)
unfold a_ai_disj in |- *.
(* Goal: forall (_ : forall (i : Int) (_ : LOOKUP unit i (AVL_intro unit a avl_a) tt) (bs : nf_list) (_ : LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs), False) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) (AVL_intro unit a' avl_a')) (_ : forall bs : nf_list, not (LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs)) (i : Int) (_ : LOOKUP unit i (AVL_intro unit a' avl_a') tt) (bs : nf_list) (_ : LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs), False *)
simpl in |- *.
(* Goal: forall (_ : forall (i : Int) (_ : lookup unit i a tt) (bs : nf_list) (_ : lookup nf_list i ai bs), False) (_ : forall d : unit, not (lookup unit i a d)) (_ : equiv_ins nf_list i (@cons normal_form b) nf_nil ai ai') (i : Int) (_ : lookup unit i a tt) (bs : nf_list) (_ : lookup nf_list i ai' bs), False *)
intros a_ai_disj0 not_lookup_i equiv_ins j lookup_j bs lookup_bs.
(* Goal: False *)
elim (equal_dec j i).
(* Goal: forall _ : Equal j i, False *)
(* Goal: forall _ : not (Equal j i), False *)
intros equal_ji.
(* Goal: False *)
(* Goal: forall _ : not (Equal j i), False *)
apply (not_lookup_i tt).
(* Goal: lookup unit i a tt *)
(* Goal: forall _ : not (Equal j i), False *)
 rewrite <- (equal_eq j i); assumption.
(* Goal: forall _ : not (Equal j i), False *)
intros not_equal_ji.
(* Goal: False *)
apply a_ai_disj0 with j bs; clear a_ai_disj0; try assumption.
(* Goal: lookup unit i0 a tt *)
(* Goal: lookup nf_list i0 ai bs0 *)
inversion_clear equiv_ins.
(* Goal: lookup unit i0 a tt *)
(* Goal: lookup nf_list i0 ai bs0 *)
apply H2; assumption.
Qed.



Lemma disjs_delete_ai :
 forall (i : Int) (a a' : atoms) (ai ai' : atomic_imps),
 a_ai_disj a ai ->
 EQUIV_INS unit i (fun _ : unit => tt) tt a a' ->
 EQUIV_DEL nf_list i ai ai' -> a_ai_disj a' ai'.
(* Goal: forall (i : Int) (a a' : atoms) (ai ai' : atomic_imps) (_ : a_ai_disj a ai) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a') (_ : EQUIV_DEL nf_list i ai ai'), a_ai_disj a' ai' *)
intros i a a' ai ai'.
(* Goal: forall (_ : a_ai_disj a ai) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a') (_ : forall bs : nf_list, not (LOOKUP nf_list i ai bs)), a_ai_disj a' ai *)
elim a; clear a; intros a avl_a.
(* Goal: forall (_ : a_ai_disj (AVL_intro unit a avl_a) ai) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) a') (_ : forall bs : nf_list, not (LOOKUP nf_list i ai bs)), a_ai_disj a' ai *)
elim a'; clear a'; intros a' avl_a'.
(* Goal: forall (_ : a_ai_disj (AVL_intro unit a avl_a) ai) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) (AVL_intro unit a' avl_a')) (_ : forall bs : nf_list, not (LOOKUP nf_list i ai bs)), a_ai_disj (AVL_intro unit a' avl_a') ai *)
elim ai; clear ai; intros ai avl_ai.
(* Goal: forall (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) (AVL_intro unit a' avl_a')) (_ : EQUIV_DEL nf_list i (AVL_intro nf_list ai avl_ai) ai'), a_ai_disj (AVL_intro unit a' avl_a') ai' *)
elim ai'; clear ai'; intros ai' avl_ai'.
(* Goal: forall (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) (AVL_intro unit a' avl_a')) (_ : forall bs : nf_list, not (LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs)), a_ai_disj (AVL_intro unit a' avl_a') (AVL_intro nf_list ai avl_ai) *)
unfold a_ai_disj in |- *.
(* Goal: forall (_ : forall (i : Int) (_ : LOOKUP unit i (AVL_intro unit a avl_a) tt) (bs : nf_list) (_ : LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs), False) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) (AVL_intro unit a' avl_a')) (_ : forall bs : nf_list, not (LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs)) (i : Int) (_ : LOOKUP unit i (AVL_intro unit a' avl_a') tt) (bs : nf_list) (_ : LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs), False *)
simpl in |- *.
(* Goal: forall (_ : forall (i : Int) (_ : lookup unit i a tt) (bs : nf_list) (_ : lookup nf_list i ai bs), False) (_ : equiv_ins unit i (fun _ : unit => tt) tt a a') (_ : equiv_del nf_list i ai ai') (i : Int) (_ : lookup unit i a' tt) (bs : nf_list) (_ : lookup nf_list i ai' bs), False *)
intros a_ai_disj0 equiv_ins equiv_del i0 lookup_j bs0 lookup_bs0.
(* Goal: False *)
elim (equal_dec i0 i).
(* Goal: forall _ : Equal i0 i, False *)
(* Goal: forall _ : not (Equal i0 i), False *)
intro equal_i.
(* Goal: lookup nf_list i0 ai bs0 *)
inversion_clear equiv_del.
(* Goal: False *)
(* Goal: forall _ : not (Equal i0 i), False *)
apply H with i0 bs0; assumption.

(* Goal: forall _ : not (Equal i0 i), False *)
intros not_equal_i.
(* Goal: False *)
apply a_ai_disj0 with i0 bs0.
(* Goal: lookup unit i0 a tt *)
(* Goal: lookup nf_list i0 ai bs0 *)
inversion_clear equiv_ins.
(* Goal: lookup unit i0 a tt *)
(* Goal: lookup nf_list i0 ai bs0 *)
apply H2; assumption.
(* Goal: lookup nf_list i0 ai bs0 *)
inversion_clear equiv_del.
(* Goal: lookup nf_list i0 ai bs0 *)
apply H1; assumption.
Qed.



Lemma goal_disj_insert_a :
 forall (i goal : Int) (a a' : atoms),
 a_goal_disj a goal ->
 (Equal goal i -> False) ->
 EQUIV_INS unit i (fun _ : unit => tt) tt a a' -> a_goal_disj a' goal.
(* Goal: forall (i goal : Int) (a a' : atoms) (_ : a_goal_disj a goal) (_ : forall _ : Equal goal i, False) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a'), a_goal_disj a' goal *)
intros i goal a a'.
(* Goal: forall (_ : a_ai_disj a ai) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a') (_ : forall bs : nf_list, not (LOOKUP nf_list i ai bs)), a_ai_disj a' ai *)
elim a; clear a; intros a avl_a.
(* Goal: forall (_ : a_ai_disj (AVL_intro unit a avl_a) ai) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) a') (_ : forall bs : nf_list, not (LOOKUP nf_list i ai bs)), a_ai_disj a' ai *)
elim a'; clear a'; intros a' avl_a'.
(* Goal: forall (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : forall _ : Equal goal i, False) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) (AVL_intro unit a' avl_a')), a_goal_disj (AVL_intro unit a' avl_a') goal *)
unfold a_goal_disj in |- *.
(* Goal: forall (_ : forall (i : Int) (_ : LOOKUP unit i (AVL_intro unit a avl_a) tt) (bs : nf_list) (_ : LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs), False) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) (AVL_intro unit a' avl_a')) (_ : forall bs : nf_list, not (LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs)) (i : Int) (_ : LOOKUP unit i (AVL_intro unit a' avl_a') tt) (bs : nf_list) (_ : LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs), False *)
simpl in |- *.
(* Goal: forall (_ : forall _ : lookup unit goal a tt, False) (_ : forall _ : Equal goal i, False) (_ : equiv_ins unit i (fun _ : unit => tt) tt a a') (_ : lookup unit goal a' tt), False *)
intros a_goal_disj0 not_equal equiv_ins lookup.
(* Goal: False *)
apply a_goal_disj0.
(* Goal: lookup unit i0 a tt *)
(* Goal: lookup nf_list i0 ai bs0 *)
inversion_clear equiv_ins.
(* Goal: lookup unit i0 a tt *)
(* Goal: lookup nf_list i0 ai bs0 *)
apply H2; assumption.
Qed.



Lemma disjs_insert_a :
 forall (i : Int) (a a' : atoms) (ai : atomic_imps),
 a_ai_disj a ai ->
 EQUIV_INS unit i (fun _ : unit => tt) tt a a' ->
 (forall bs : nf_list, ~ LOOKUP nf_list i ai bs) -> a_ai_disj a' ai.
(* Goal: forall (i : Int) (a a' : atoms) (ai : atomic_imps) (_ : a_ai_disj a ai) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a') (_ : forall bs : nf_list, not (LOOKUP nf_list i ai bs)), a_ai_disj a' ai *)
intros i a a' ai.
(* Goal: forall (_ : a_ai_disj a ai) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a') (_ : forall bs : nf_list, not (LOOKUP nf_list i ai bs)), a_ai_disj a' ai *)
elim a; clear a; intros a avl_a.
(* Goal: forall (_ : a_ai_disj (AVL_intro unit a avl_a) ai) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) a') (_ : forall bs : nf_list, not (LOOKUP nf_list i ai bs)), a_ai_disj a' ai *)
elim a'; clear a'; intros a' avl_a'.
(* Goal: forall (_ : a_ai_disj (AVL_intro unit a avl_a) ai) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) (AVL_intro unit a' avl_a')) (_ : forall bs : nf_list, not (LOOKUP nf_list i ai bs)), a_ai_disj (AVL_intro unit a' avl_a') ai *)
elim ai; clear ai; intros ai avl_ai.
(* Goal: forall (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) (AVL_intro unit a' avl_a')) (_ : forall bs : nf_list, not (LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs)), a_ai_disj (AVL_intro unit a' avl_a') (AVL_intro nf_list ai avl_ai) *)
unfold a_ai_disj in |- *.
(* Goal: forall (_ : forall (i : Int) (_ : LOOKUP unit i (AVL_intro unit a avl_a) tt) (bs : nf_list) (_ : LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs), False) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit a avl_a) (AVL_intro unit a' avl_a')) (_ : forall bs : nf_list, not (LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs)) (i : Int) (_ : LOOKUP unit i (AVL_intro unit a' avl_a') tt) (bs : nf_list) (_ : LOOKUP nf_list i (AVL_intro nf_list ai avl_ai) bs), False *)
simpl in |- *.
(* Goal: forall (_ : forall (i : Int) (_ : lookup unit i a tt) (bs : nf_list) (_ : lookup nf_list i ai bs), False) (_ : equiv_ins unit i (fun _ : unit => tt) tt a a') (_ : forall bs : nf_list, not (lookup nf_list i ai bs)) (i : Int) (_ : lookup unit i a' tt) (bs : nf_list) (_ : lookup nf_list i ai bs), False *)
intros a_ai_disj0 equiv_ins not_lookup_bs i0 lookup_j bs0 lookup_bs0.
(* Goal: False *)
elim (equal_dec i0 i).
(* Goal: forall _ : Equal i0 i, False *)
(* Goal: forall _ : not (Equal i0 i), False *)
intro equal_i.
(* Goal: False *)
(* Goal: forall _ : not (Equal i0 i), False *)
apply (not_lookup_bs bs0).
(* Goal: lookup nf_list i ai bs0 *)
(* Goal: forall _ : not (Equal i0 i), False *)
 rewrite <- (equal_eq i0 i); assumption.

(* Goal: forall _ : not (Equal i0 i), False *)
intros not_equal_i.
(* Goal: False *)
apply a_ai_disj0 with i0 bs0.
(* Goal: lookup unit i0 a tt *)
(* Goal: lookup nf_list i0 ai bs0 *)
inversion_clear equiv_ins.
(* Goal: lookup unit i0 a tt *)
(* Goal: lookup nf_list i0 ai bs0 *)
apply H2; assumption.
(* Goal: lookup nf_list i0 ai bs0 *)
assumption.
Qed.
