Require MinMJ_F.
Require PolyList.
Require MinMJ_Syntax.

(* Syntactic Definition Hyps := (list F). *)

Grammar command command3 :=
	["Hyps"] -> [$0=<<(list F)>>].

Syntax constr HYPS <<(list F)>> 3
	"Hyps".

(* Syntactic Definition MT := (nil F). *)

Grammar command command3 :=
	["MT"] -> [$0=<<(nil F)>>].

Syntax constr NH <<(nil F)>> 3
	"MT".

(* Syntactic Definition Add_Hyp := (cons F). *)

Grammar command command3 :=
	["Add_Hyp" command:command($f) command:command($h)] ->
	[$0 = <<(cons F $f $h)>>].

Syntax constr AH <<(cons F $f $h)>> 3
	"Add_Hyp " <$f:"term":L> " " <$h:"term":E>.

Grammar command command3 :=
	["Len_Hyps" command:command($h)] ->
	[$0 = <<(length F $h)>>].

Syntax contr LH <<(length F $h)>> 3
	"Len_Hyps " <$h:"term":E>.

Lemma Add_Hyp1 :
	(i:Hyps)(P:F)~(Add_Hyp P i)=i.

(Induction i; Clear  i; Intros).
Discriminate.

(Unfold not; Intros; Apply (H a)).
(Injection H0; Auto).
Save.

Hint Add_Hyp1.

Recursive Definition
    Hypseqb : Hyps->Hyps->bool :=
	MT MT => true |
	MT (Add_Hyp P' h') => false |
	(Add_Hyp P h) MT => false |
	(Add_Hyp P h) (Add_Hyp P' h') => (andb (Feqb P P') (Hypseqb h h')).

Lemma Hypseqb_sym :
	(i,j:Hyps)(Hypseqb i j)=(Hypseqb j i).

(Induction i; Clear  i; Induction j; Clear  j; Intros; Simpl;
 Try Trivial).
(Rewrite -> Feqb_sym; Rewrite -> (H l0); Auto).
Save.

Lemma Hypseqb_is_eq1 :
	(i,j:Hyps)i=j->(Hypseqb i j)=true.

(Intros; Rewrite -> H; Elim j; Clear  H j; Intros; Auto).
(Simpl; Rewrite -> Feqb_is_eq1; Auto; Rewrite -> H; Auto).
Save.

Lemma Hypseqb_is_eq2 :
	(i,j:Hyps)(Hypseqb i j)=true->i=j.

(Induction i; Clear  i; Induction j; Clear  j; Intros; Auto).
Discriminate H0.

Discriminate H0.

Simpl in H1.
Clear  H0.
Cut (Feqb a a0)=true.
Intros.
Cut (Hypseqb l l0)=true.
Intros.
(Rewrite -> (Feqb_is_eq2 a a0); Auto).
(Rewrite -> (H l0); Auto).

(Generalize H1 ; Clear  H1; Case (Hypseqb l l0); Rewrite -> H0; Auto).

(Generalize H1 ; Clear  H1; Case (Feqb a a0); Auto).
Save.

Lemma Hypseqb_is_eq3 :
	(i,j:Hyps)(~i=j)->(Hypseqb i j)=false.

(Unfold not; Intros; Apply bool_dec5; Unfold not; Intros; Apply H;
 Apply Hypseqb_is_eq2; Auto).
Save.

Lemma Hypseqb_is_eq4 :
	(i,j:Hyps)(Hypseqb i j)=false->~i=j.

Intros; Cut ~(Hypseqb i j)=true.
Unfold not; Intros; Apply H0; Apply (Hypseqb_is_eq1 i j H1).

Apply bool_dec6; Auto.
Save.

Definition Hyps_compare1 : Hyps->Hyps->Prop :=
[i,j:Hyps]((Hypseqb i j)=true)\/(Hypseqb i j)=false.

Lemma Hypseqb_dec :
	(i,j:Hyps)(Hyps_compare1 i j).

Unfold Hyps_compare1.
Intros; Case (Hypseqb i j); Auto.
Save.

Definition Hyps_compare :Hyps->Hyps->Prop :=
	[i,j:Hyps]i=j\/~i=j.

Lemma Hypseq_dec :
	(i,j:Hyps)(Hyps_compare i j).

Unfold Hyps_compare.
Intros.
Cut (Hyps_compare1 i j).
Unfold Hyps_compare1.
Intros c;Elim c;[Clear  c;Intros c|Clear  c;Intros c].
Left.
Apply (Hypseqb_is_eq2 i j c).

Right.
Apply Hypseqb_is_eq4.
Auto.

Exact (Hypseqb_dec i j).
Save.