Require EqDecide.
Require Arith.
Require Peano_dec.
Require Zerob.
Require PolyList.
Require sem_ex.
Require relation.
Section Exclusion_mutuelle.
Definition T := (1).
Definition F := (0).
Inductive var_ex : Set := pc1 : var_ex | pc2 : var_ex | tour : var_ex.
Definition cte_ex := nat.
Inductive fun_ex : Set := f_eq : fun_ex | f_conj : fun_ex | f_or : fun_ex.
Definition term':= (term var_ex cte_ex fun_ex).
Definition Var' := (!Var var_ex cte_ex fun_ex).
Definition Cte' := (!Cte var_ex cte_ex fun_ex).
Definition Fun' := (!Fun var_ex cte_ex fun_ex).
Definition Vpc1 := (Var' pc1).
Definition Vpc2 := (Var' pc2).
Definition Vtour := (Var' tour).
Definition Cte_n := [n:nat](Cte' n).
Definition F_eq := (Fun' f_eq).
Definition F_conj := (Fun' f_conj).
Definition F_or := (Fun' f_or).
Definition eq_var_ex_dec : (v,v':var_ex){v=v'}+{~v=v'}.
Decide Equality.
Defined.
Definition cte_ex_sem : cte_ex -> nat := [n]n.
Definition fun_ex_sem : fun_ex -> nat -> nat -> nat
:= [f][n,m]Cases f of f_eq => if (eq_nat_dec n m) then [_]T else [_]F
| f_conj => if (zerob n) then F else m
| f_or => if (zerob n) then m else T
end.
Definition term_sem' := (term_sem 1!var_ex cte_ex_sem fun_ex_sem).
Lemma term_sem_f_eq_elim :
(t1,t2:term')(v:(valuation var_ex))
~(term_sem' v (F_eq t1 t2))=O -> (term_sem' v t1)=(term_sem' v t2).
Simpl; Intros t1 t2 v.
Case (eq_nat_dec (term_sem' v t1) (term_sem' v t2)); Intros; Auto.
Case H; Trivial.
Save.
Lemma term_sem_f_conj_elim :
(t1,t2:term')(v:(valuation var_ex))
~(term_sem' v (F_conj t1 t2))=O
-> ~(term_sem' v t1)=O /\ ~(term_sem' v t2)=O.
Simpl; Intros t1 t2 v.
Case (term_sem' v t1); Intros; Auto.
Save.
Lemma term_sem_f_or_elim :
(t1,t2:term')(v:(valuation var_ex))
~(term_sem' v (F_or t1 t2))=O
-> ~(term_sem' v t1)=O \/ ~(term_sem' v t2)=O.
Simpl; Intros t1 t2 v.
Case (term_sem' v t1); Intros; Auto.
Save.
Definition c1
:= ((F_eq Vpc1 (Cte_n (1))),
(cons (pc1,(Cte_n (2))) (cons (tour,Cte_n F) (nil ?)))).
Definition c2
:= ((F_conj (F_eq Vpc1 (Cte_n (2)))
(F_or (F_eq Vpc2 (Cte_n (1))) (F_eq Vtour (Cte_n T)))),
(cons (pc1,(Cte_n (3))) (nil ?))).
Definition c3 := ((F_eq Vpc1 (Cte_n (3))), (cons (pc1,(Cte_n (1))) (nil ?))).
Definition d1 := ((F_eq Vpc2 (Cte_n (1))),
(cons (pc2,(Cte_n (2))) (cons (tour,Cte_n T) (nil ?)))).
Definition d2 := ((F_conj (F_eq Vpc2 (Cte_n (2)))
(F_or (F_eq Vpc1 (Cte_n (1)))
(F_eq Vtour (Cte_n F)))),
(cons (pc2,(Cte_n (3))) (nil ?))).
Definition d3 := ((F_eq Vpc2 (Cte_n (3))),
(cons (pc2,(Cte_n (1))) (nil ?))).
Lemma not_eq_T_F : (x:nat)(x=T)->(x=F)->False.
Intros x H; Rewrite H; Discriminate.
Save.
Lemma not_eq_1_2 : (x:nat)(x=(1))->(x=(2))->False.
Intros x H; Rewrite H; Discriminate.
Save.
Lemma not_eq_1_3 : (x:nat)(x=(1))->(x=(3))->False.
Intros x H; Rewrite H; Discriminate.
Save.
Lemma not_eq_2_3 : (x:nat)(x=(2))->(x=(3))->False.
Intros x H; Rewrite H; Discriminate.
Save.
Inductive init_ex [v:(valuation var_ex)] : Prop :=
init_ex_intro : (v pc1)=(1) -> (v pc2)=(1) -> (v tour)=T -> (init_ex v).
Definition prog_ex
:= (cons c1 (cons c2 (cons c3 (cons d1 (cons d2 (cons d3 (nil ?))))))).
Definition trans_ex
:= (trans_prog cte_ex_sem fun_ex_sem eq_var_ex_dec prog_ex).
| Premier invariant qui restreint le domaine des variables |
Inductive type_pc : nat -> Prop :=
pc_1 : (type_pc (1))
| pc_2 : (type_pc (2))
| pc_3 : (type_pc (3)).
Hint type_pc_constr := Constructors type_pc.
Inductive type_tour : nat -> Prop :=
tour_0 : (type_tour (0))
| tour_1 : (type_tour (1)).
Hint type_tour_constr := Constructors type_tour.
Inductive type_inv [v:(valuation var_ex)] : Prop :=
type_inv_intro
: (type_pc (v pc1)) -> (type_pc (v pc2)) -> (type_tour (v tour)) -> (type_inv v).
Transparent eq_nat_dec.
Lemma type_inv_lemma :
(v:(valuation var_ex))(accessible trans_ex init_ex v)->(type_inv v).
Intros v a; Elim a; Clear a v.
Destruct 1; Split; Auto.
Rewrite H0; Trivial.
Rewrite H1; Trivial.
Rewrite H2; Trivial.
Intros v _ tv v' trans.
Generalize tv; Case trans.
Simpl; Intros c H3; Decompose Sum H3.
Rewrite <-H; Intros (G1,G2); Rewrite <- G2; Clear G2; Destruct 1; Split; Simpl; Auto.
Rewrite <-H0; Intros (G1,G2); Rewrite <- G2; Clear G2; Destruct 1; Split; Simpl; Auto.
Rewrite <-H; Intros (G1,G2); Rewrite <- G2; Clear G2; Destruct 1; Split; Simpl; Auto.
Rewrite <-H0; Intros (G1,G2); Rewrite <- G2; Clear G2; Destruct 1; Split; Simpl; Auto.
Rewrite <-H; Intros (G1,G2); Rewrite <- G2; Clear G2; Destruct 1; Split; Simpl; Auto.
Rewrite <-H0; Intros (G1,G2); Rewrite <- G2; Clear G2; Destruct 1; Split; Simpl; Auto.
Save.
Definition section_critique [v:(valuation var_ex)] : Prop :=
~((v pc1)=(3) /\ (v pc2)=(3)).
Inductive section_critique_gen [v:(valuation var_ex)] : Prop :=
scrit_intro :
((v pc1)=(3) -> ((v pc2)=(1) \/ ((v pc2) = (2) /\ ((v tour)=T))))
-> ((v pc2)=(3) -> ((v pc1)=(1) \/ ((v pc1) = (2) /\ ((v tour)=F))))
-> (section_critique_gen v).
| Tous les états accessibles satisfont la propriété de section critique |
Lemma accessible_sec_crit :
(v:(valuation var_ex))(accessible trans_ex init_ex v)->(section_critique v).
Intros.
Cut (section_critique_gen v).
(section_critique_gen v) -> (section_critique v)
|
Repeat Red; Intros gen (H1,H2).
Case gen; Auto; Intros.
Case H0; Trivial; Intros.
Apply (not_eq_1_3 (v pc2)); Trivial.
Case H4; Intros; Apply (not_eq_2_3 (v pc2)); Trivial.
Elim H; Clear H; Clear v.
| cas initial |
Destruct 1; Split; Intros.
Case (not_eq_1_3 (m pc1)); Trivial.
Case (not_eq_1_3 (m pc2)); Trivial.
| cas inductif |
Intros v1 accv1 scv1 v2 trans; Case trans; Clear trans.
Case scv1; Clear scv1; Intros scv1 scv2.
Intros x pr; Simpl in pr; Decompose Sum pr; Clear pr; Simpl.
Case H; Intros.
Case H0; Clear H0; Simpl; Intros garde upd.
Case upd; Clear upd; Split; Simpl; Intros.
Discriminate H0.
Auto.
Case H0; Clear H0 x; Intros.
Case H; Clear H; Intros garde upd.
Case upd; Clear upd.
Clear H; Case term_sem_f_conj_elim with 1:=garde; Clear garde; Intros.
Assert H3 := (term_sem_f_eq_elim ? ? ? H); Clear H; Simpl in H3.
Case term_sem_f_or_elim with 1:=H0; Clear H0; Intros.
Assert H2 := (term_sem_f_eq_elim ? ? ? H); Clear H; Simpl in H2.
Split; Simpl; Intros; Auto.
Case (not_eq_1_3 (v1 pc2)); Trivial.
Assert H2 := (term_sem_f_eq_elim ? ? ? H); Clear H; Simpl in H2.
Split; Simpl; Intros; Auto.
Case (type_inv_lemma v1 accv1); Intros.
Inversion H1; Auto.
Case scv2; Auto; Intros.
Case (not_eq_1_2 (v1 pc1)); Trivial.
Case H5; Intros.
Case (not_eq_T_F (v1 tour)); Trivial.
Case scv2; Auto; Intros.
Case (not_eq_1_2 (v1 pc1)); Trivial.
Case H0; Clear H0; Intros.
Case (not_eq_1_2 (v1 pc1)); Trivial.
Case (not_eq_T_F (v1 tour)); Trivial.
Case H; Clear H x; Intros.
Case H; Clear H; Intros garde upd.
Case upd; Clear upd.
Assert H1 := (term_sem_f_eq_elim ? ? ? garde); Clear garde; Simpl in H1.
Case scv1; Intros; Auto.
Split; Simpl; Intros; Auto.
Split; Simpl; Intros; Auto.
Case H0; Intros.
Case H; Clear H; Simpl; Intros garde upd.
Case upd; Clear upd; Split; Simpl; Intros.
Auto.
Discriminate H.
Case H; Clear H x; Intros.
Case H; Clear H; Intros garde upd.
Case upd; Clear upd.
Clear H; Case term_sem_f_conj_elim with 1:=garde; Clear garde; Intros.
Assert H3 := (term_sem_f_eq_elim ? ? ? H); Clear H; Simpl in H3.
Case term_sem_f_or_elim with 1:=H0; Clear H0; Intros.
Assert H2 := (term_sem_f_eq_elim ? ? ? H); Clear H; Simpl in H2.
Split; Simpl; Intros; Auto.
Case (not_eq_1_3 (v1 pc1)); Trivial.
Assert H2 := (term_sem_f_eq_elim ? ? ? H); Clear H; Simpl in H2.
Split; Simpl; Intros; Auto.
Case scv1; Auto; Intros.
Case (not_eq_1_2 (v1 pc2)); Trivial.
Case H0; Intros.
Case (not_eq_T_F (v1 tour)); Trivial.
Clear H; Case (type_inv_lemma v1 accv1); Intros.
Inversion H; Auto.
Case scv1; Auto; Intros.
Case (not_eq_1_2 (v1 pc2)); Trivial.
Case H4; Intros.
Case (not_eq_T_F (v1 tour)); Trivial.
Case H0; Clear H0 x; Intros.
Case H; Clear H; Intros garde upd.
Case upd; Clear upd.
Assert H1 := (term_sem_f_eq_elim ? ? ? garde); Clear garde; Simpl in H1.
Case scv2; Intros; Auto.
Split; Simpl; Intros; Auto.
Split; Simpl; Intros; Auto.
Save.