Integrated Subtyping (Preprocess.v)
To specify integrated subtyping, the user supplies an integrator i, and integrated-predicate Preprocessed, subject to a few requirements:- counit: the result of integrating a type must be a reductive subtype of the original type. This corresponds to the "Literal Dereliction" requirement in the paper. The full "Dereliction" Lemma easily follows from transitivity.
- i_preprocessed: the result of integrating a type must be integrated according to the integrated-predicate Preprocessed. This corresponds to the "Integrator Integrated" Lemma in the paper; which just lifts the "Intersector Integrated" requirement to dnf and unions/intersection types.
- Opt: Intuitively, integrated subtyping integrates the LHS type at every recursive step in subtyping. However, there are many subtyping rules that have premises whose LHS is integrated if the LHS of the conclusion is integrated. In this case, we can optimize those subtyping rules to not integrate the LHS (see the definition of Ass in PreprocessingRules). In the paper, we use this insight to only apply the integrator at the beginning of subtyping, and then the intersector whenever we recurse trough literals. This is because for the intersection and union subtyping rules, the LHS is essentially always integrated. In order for this to be true for LHS-intersection rule, the formalization here would require that if an intersection is integrated, so are both of its components. For the system in the paper, we relaxed this requirement - this is the small relaxation we allude to in section 7.
- i_promote_R: a proof of promotion, corresponding roughly to the "Literal Promotion" requirement in the paper, but using a general relation R that just admits the decidable rules, reflexivity, and monotonicity (as we alluded to in section 7) in order to model proofs with assumptions.
- i_wf: the new subtyping relation must still be well-founded. In the paper, we prove this from the "Measure Preservation" requirement, which in this case comes down to proving well-foundedness of the subtyping relation altogether
Require Import Common.
Require Import Decide.
Require Import Coq.Lists.List.
Module Type Comonad (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule).
Import T.
Import Rule.
Module Decidable := Decidable T Rule ORule DRule.
Import Decidable.
Parameter i : T -> T.
Parameter counit : forall t : T, Decidable (i t) t.
Parameter Preprocessed : T -> Prop.
Parameter i_preprocessed : forall t : T, Preprocessed (i t).
Parameter Opt : forall {t t' : T} {con : Con t t'} (req : Req con), option (Preprocessed t -> Preprocessed (Ass req left)).
Parameter i_promote_R : forall R : T -> T -> Prop, (forall t, R t t) -> (forall t1 t2 t3 t4 : T, Decidable t1 t2 -> R t2 t3 -> Decidable t3 t4 -> R t1 t4) -> AdmitsD R -> Decidable.Proof.Inverts Preprocessed R -> forall (t t' : T) (con : Con t t'), Preprocessed t -> (forall req : Req con, R (Rule.Ass req left) (Rule.Ass req right)) -> (forall req : Req con, Preprocessed (Ass req left) -> R (Ass req left) (i (Ass req right))) -> R t (i t').
End Comonad.
Module PreprocessingRules (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule) (I : Comonad T Rule ORule DRule) <: Rules T.
Import T.
Import I.
Definition Con := Rule.Con.
Definition Req : forall {t t' : T}, Con t t' -> Type
:= @Rule.Req.
Definition Ass : forall {t t' : T} {con : Con t t'}, Req con -> Position -> T
:= fun t t' con req pos => match pos with
| left => match Opt req with
| None => i (Rule.Ass req left)
| Some _ => Rule.Ass req left
end
| right => Rule.Ass req right
end.
Definition Var : forall {t t' : T} {con : Con t t'}, Req con -> Variance := @ORule.Var.
End PreprocessingRules.
Module Type WellFoundedComonad (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule) (I : Comonad T Rule ORule DRule).
Import T.
Import Rule.
Import I.
Module PRule := PreprocessingRules T Rule ORule DRule I.
Import PRule.
Parameter i_wf : forall (R : T -> T -> Type), (forall t1 t2 : T, (forall (con : Con t1 t2) (req : Req con), R (Ass req left) (Ass req right)) -> R t1 t2) -> forall t t' : T, R t t'.
End WellFoundedComonad.
Module Preprocessing (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule) (I : Comonad T Rule ORule DRule) (WFI : WellFoundedComonad T Rule ORule DRule I).
Import T.
Import I.
Import WFI.
Module PRule := WFI.PRule.
Import PRule.
Module ProofPV := ProofPV T PRule PRule.
Import ProofPV.
Module Proof := ProofPV.Proof.
Import Proof.
Module Decidable := I.Decidable.
Import Decidable.
Definition Preprocessing := Proof.
Section PreprocessingDecidable.
Local Definition drefl := DRule.refl.
Local Definition dtrans : forall {t1 t2 t3 : T}, Decidable t1 t2 -> Decidable t2 t3 -> Decidable t1 t3 := @Decidable.trans.
Lemma dderelict {t t' : T} : Decidable t t' -> Decidable (i t) t'.
apply dtrans. apply counit.
Qed.
Lemma dpromote' {t t' : T} : Preprocessed t -> Decidable t t' -> Decidable t (i t').
intros pre d. revert pre. induction d as [ t t' con ass rec ]. intro pre. apply i_promote_R with con; try clear t t' con ass rec pre.
exact DRule.refl.
intros t1 t2 t3 t4 d d'. apply dtrans. revert d d'. apply dtrans.
apply Decidable.Proof.proof_admits.
intros t t' pre d. induction d as [ t t' con ass rec ]. apply Decidable.Proof.inversion with con; assumption.
assumption.
assumption.
assumption.
Qed.
Corollary dpromote {t t' : T} : Decidable (i t) t' -> Decidable (i t) (i t').
apply dpromote'. apply i_preprocessed.
Qed.
Corollary dpreprocessed {t : T} : Preprocessed t -> Decidable t (i t).
intro pre. apply dpromote'; try assumption. apply drefl.
Qed.
Corollary dmap {t t' : T} : Decidable t t' -> Decidable (i t) (i t').
intro d. apply dpromote. apply dderelict. assumption.
Qed.
End PreprocessingDecidable.
Section PreprocessingDecidableTrans.
Local Definition DecidableP := Decidable.Proof.ProofP.
Local Definition DecidablePV := Decidable.ProofPV.ProofPV.
Local Definition dpermitV := Decidable.ProofPV.permitV.
Local Definition dmonoV := @Decidable.ProofPV.monoV.
Local Definition dbindV := @Decidable.ProofPV.bindV.
Local Definition decidable_decidablePV := Decidable.ProofPV.proof_proofPV.
Local Definition decidablePV_decidable := @Decidable.ProofPV.proofPV_proof.
Local Definition decidableP_decidablePV := @Decidable.ProofPV.proofP_proofPV.
Local Definition decidablePV_decidableP := @Decidable.ProofPV.proofPV_proofP.
Import Decidable.Reduction.
Lemma decidableP_preprocessing {t1 t4 : T} : Preprocessed t1 -> DecidableP (fun t2 t3 => forall t1 t4 : T, Preprocessed t1 -> Decidable t1 t2 -> Decidable t3 t4 -> Preprocessing t1 t4) t1 t4 -> Preprocessing t1 t4.
apply (fun R rec => i_wf R rec t1 t4). clear t1 t4. intros t1 t4 rec id1 progress. simpl in rec. revert progress. generalize covariant. intros v progress. destruct progress as [ t1 t4 trans | t1 t4 con ass ].
apply trans; try trivial; try apply drefl.
apply (proof con). fold Preprocessing. intro req. apply rec.
destruct (Opt req) as [ preserve | ].
apply preserve. assumption.
apply i_preprocessed.
pose proof (ass req) as progress. clear ass rec id1 v. destruct (Opt req) as [ _ | ]; try assumption. apply (@decidablePV_decidableP covariant). pose proof (counit (Rule.Ass req left)) as d. apply (decidable_decidablePV covariant) in d. apply (decidableP_decidablePV covariant) in progress. generalize (Decidable.transPV d progress). clear d progress. apply dbindV. clear t1 t4 con req. intros v t1 t4 trans. apply trans_decidel in trans; [ | intros v' t t' f; destruct f ]. revert trans. apply dmonoV. clear v t1 t4. intros v t2 t3 coma t1 t4 it1 d1 d4. destruct v; [ destruct coma as [ t d trans ] | destruct coma as [ t trans d' ] ].
apply trans; try trivial. revert d1 d. apply dtrans.
apply trans; try trivial. revert d' d4. apply dtrans.
Qed.
Theorem decidable_trans {t1 t2 t3 t4 : T} : Preprocessed t1 -> Decidable t1 t2 -> Preprocessing t2 t3 -> Decidable t3 t4 -> Preprocessing t1 t4.
revert t1 t4. apply (fun R rec => i_trace_ind R rec t2 t3). clear t2 t3. intros t2 t3 rec t1 t4 it1 d ed d'. induction ed as [ t2 t3 mcon mass mrec ]. fold Preprocessing in mass. pose proof (rec mcon) as rec. destruct d as [ t1 t2 lcon lass ]. pose proof (DRule.Red lcon mcon) as lmact. destruct lmact as [ mreq mvar lmact e | lmcon lmact ].
pose proof (mrec mreq) as mrec. apply mrec.
intros mcon' mreq' t2' t3' trace. apply rec with mreq. revert trace. apply trace_comp'. apply recursion with mcon' mreq'. apply assumption.
unfold Ass. destruct (Opt mreq) as [ _ | ].
apply (@decidablePV_decidable covariant). revert lmact. apply dbindV. intros v t t' lreq. destruct lreq as [ lreq ]. apply decidable_decidablePV. apply lass.
apply dpromote'; try assumption. apply (@decidablePV_decidable covariant). revert lmact. apply dbindV. intros v t t' lreq. destruct lreq as [ lreq ]. apply decidable_decidablePV. apply lass.
unfold Ass. rewrite e. assumption.
clear mrec. assert (forall (v : Variance) (t2 t3 : T) (mreq : Requires mcon v t2 t3) (t1 t4 : T), Preprocessed t1 -> Decidable t1 t2 -> Decidable t3 t4 -> Preprocessing t1 t4) as rec'.
clear lass d' lmcon lmact t1 t4 lcon it1. intros v t2' t3' mreq t1 t4 it1 d d'. destruct mreq as [ mreq ]. apply rec with mreq (Ass mreq left) (Ass mreq right); try assumption.
apply assumption.
unfold Ass. destruct (Opt mreq) as [ _ | ]; try apply dpromote'; assumption.
apply mass.
clear rec. rename rec' into rec. destruct d' as [ t3 t4 rcon rass ]. pose proof (Decidable.Red' lmcon rcon) as act. apply decidableP_preprocessing; try assumption. clear it1. assert (forall (v : Variance) (t3' t4' : T), Requires rcon v t3' t4' -> Decidable t3' t4') as rass'.
intros v t3' t4' rreq. destruct rreq as [ rreq ]. apply rass.
clear rass. rename rass' into rass. assert (forall (v : Variance) (t1' t2' : T), Requires lcon v t1' t2' -> Decidable t1' t2') as lass'.
intros v t1' t2' lreq. destruct lreq as [ lreq ]. apply lass.
clear lass. rename lass' into lass. assert (forall (v : Variance) (t2 t4 : T), Requires lmcon v t2 t4 -> DecidablePV (fun _ t2 t3 => forall t1 t4 : T, Preprocessed t1 -> Decidable t1 t2 -> Decidable t3 t4 -> Preprocessing t1 t4) v t2 t4) as lmact'.
intros v t2' t3' lmreq. destruct lmreq as [ lmreq ]. generalize (lmact lmreq). apply dbindV. clear lmact lmreq rass rcon act lmcon. intros v t2' t4' comp. apply trans_decidel in comp; try assumption. clear lass lcon. revert comp. apply dmonoV. clear v t2' t4'. intros v t2' t4' coma. destruct v; [ destruct coma as [ t3' d mreq ] | destruct coma as [ t3' mreq d' ] ]; pose proof (rec _ _ _ mreq) as rec; clear mreq; intros t1' t5' it1' d1 d5; apply rec; try assumption.
revert d1 d. apply dtrans.
revert d' d5. apply dtrans.
clear lmact mass rec lcon mcon lass t2. rename lmact' into lmact. apply (@decidablePV_decidableP covariant). revert act. apply dbindV. intros v t1' t4' comp. apply trans_decider in comp; try assumption. clear rass rcon. revert comp. apply dbindV. clear v t1' t4'. intros v t1' t4' coma. destruct v; [ destruct coma as [ t3' lmreq d' ] | destruct coma as [ t2' d lmreq ] ]; pose proof (lmact _ _ _ lmreq) as lmact; clear lmreq lmcon t1 t3 t4.
apply (decidable_decidablePV covariant) in d'. generalize (Decidable.transPV lmact d'). clear lmact t3' d'. apply dbindV. clear t1' t4'. intros v t1 t4 trans. apply trans_decider in trans; [ | intros t t' v' f; destruct f ]. revert trans. apply dmonoV. clear v t1 t4. intros v t1 t4 coma t0 t5 it0 d0 d5. destruct v; [ destruct coma as [ t3 trans d ] | destruct coma as [ t3 d trans ] ]; apply trans; try assumption.
revert d d5. apply dtrans.
revert d0 d. apply dtrans.
apply (decidable_decidablePV contravariant) in d. generalize (Decidable.trans_contra d lmact). clear d lmact t2'. apply dbindV. clear t1' t4'. intros v t1 t4 trans. apply trans_decider in trans; [ | intros t t' v' f; destruct f ]. revert trans. apply dmonoV. clear v t1 t4. intros v t1 t4 coma t0 t5 it0 d0 d5. destruct v; [ destruct coma as [ t3 trans d ] | destruct coma as [ t3 d trans ] ]; apply trans; try assumption.
revert d d5. apply dtrans.
revert d0 d. apply dtrans.
Qed.
End PreprocessingDecidableTrans.
Section Comonad.
Lemma derelict {t t' : T} : Preprocessing t t' -> Preprocessing (i t) t'.
intro ed. apply @decidable_trans with t t'.
apply i_preprocessed.
apply counit.
assumption.
apply DRule.refl.
Qed.
Lemma admitsd : AdmitsD Preprocessing.
intros t1 t2 con ass. apply (proof con). intro req. unfold Ass. destruct (Opt req) as [ _ | ].
apply ass.
apply derelict. apply ass.
Qed.
Definition iPreprocessing (t2 t3 : T) := forall t1 t4 : T, Preprocessed t1 -> Decidable t1 t2 -> Decidable t3 t4 -> Preprocessing t1 t4.
Lemma iadmitsd : AdmitsD iPreprocessing.
intros t2 t3 con ass t1 t4 pre d d'. apply decidableP_preprocessing; try assumption. clear pre. assert (DecidableP iPreprocessing t2 t4) as dp. assert (DecidableP iPreprocessing t2 t3) as ed; [ apply @Decidable.Proof.proofP with con; intro req; apply Decidable.Proof.permit; apply ass | clear con ass ]. apply Decidable.Proof.proof_proofP in d'. revert ed d'. apply Decidable.trans_bind. clear t1 t2 t3 t4 d. intros v t1 t3 trans. apply Decidable.Proof.permit. destruct trans as [ coma | coma ].
destruct v; [ destruct coma as [ t2 l r ] | destruct coma as [ t2 l r ] ].
apply Decidable.ProofPV.proofPV_proof in r. intros t0 t5 pre d d'. apply l; try assumption. revert r d'. apply Decidable.trans.
apply Decidable.ProofPV.proofPV_proof in l. intros t0 t5 pre d d'. apply r; try assumption. revert d l. apply Decidable.trans.
destruct v; [ destruct coma as [ t2 l r ] | destruct coma as [ t2 l r ] ].
destruct r.
destruct l.
clear d' t3 con ass. apply Decidable.Proof.proof_proofP in d. revert d dp. apply Decidable.trans_bind. clear t2 t1 t4. intros v t1 t3 trans. apply Decidable.Proof.permit. destruct trans as [ coma | coma ].
destruct v; [ destruct coma as [ t2 l r ] | destruct coma as [ t2 l r ] ].
destruct l.
destruct r.
destruct v; [ destruct coma as [ t2 l r ] | destruct coma as [ t2 l r ] ].
apply Decidable.ProofPV.proofPV_proof in l. intros t0 t5 pre d d'. apply r; try assumption. revert d l. apply Decidable.trans.
apply Decidable.ProofPV.proofPV_proof in r. intros t0 t5 pre d d'. apply l; try assumption. revert r d'. apply Decidable.trans.
Qed.
Lemma decidable_preprocessing {t t' : T} : Decidable t t' -> Preprocessing t t'.
intro d. induction d as [ t t' con _ rec ]. apply (proof con). intro req. unfold Ass. destruct (Opt req) as [ _ | ]; try apply derelict; apply rec.
Qed.
Lemma refl (t : T) : Preprocessing t t.
apply decidable_preprocessing. apply DRule.refl.
Qed.
Lemma iiinverts : Decidable.Proof.Inverts Preprocessed iPreprocessing.
intros t t'. apply (fun R rec => DRule.wf R rec t t'). clear t t'. intros t1 t2 rec pre ed. pose proof (ed t1 t2 pre (drefl _) (drefl _)) as ed. clear pre. destruct ed as [ t2 t3 con ass ]. apply Decidable.Proof.inversion with con.
intros req t1 t4 pre d d'. pose proof (ass req) as ass. unfold Ass in ass. destruct (Opt req) as [ _ | ].
revert pre d ass d'. apply @decidable_trans.
apply dpromote' in d; try assumption. revert pre d ass d'. apply @decidable_trans.
intros req pre. apply rec; try assumption. clear pre. intros t1 t4 pre d d'. pose proof (ass req) as ass. unfold Ass in ass. destruct (Opt req) as [ _ | ].
revert pre d ass d'. apply @decidable_trans.
apply dpromote' in d; try assumption. revert pre d ass d'. apply @decidable_trans.
Qed.
Lemma ipromote {t2 t3 : T} : Preprocessing t2 t3 -> Preprocessed t2 -> iPreprocessing t2 (i t3).
intro ed. induction ed as [ t2 t3 con ass rec ]. intro pre. apply (i_promote_R iPreprocessing) with con; try clear t2 t3 con ass rec pre.
intros t2 t1 t3 pre d d'. apply decidable_preprocessing. revert d d'. apply Decidable.trans.
intros t1 t2 t3 t4 d ed d' t t' pre' d'' d'''. apply ed; try assumption.
revert d'' d. apply dtrans.
revert d' d'''. apply dtrans.
exact iadmitsd.
exact iiinverts.
assumption.
intros req t1 t4 pre' d d'. pose proof (ass req) as ass. revert ass d'. apply decidable_trans; try assumption. unfold Ass. destruct (Opt req) as [ _ | ]; try apply dpromote'; assumption.
clear ass pre. intros req pre t1 t4 pre' d d'. apply rec with req; try assumption.
unfold Ass. destruct (Opt req) as [ _ | ]; try assumption. apply i_preprocessed.
unfold Ass. destruct (Opt req) as [ _ | ]; try assumption. apply dpromote'; assumption.
Qed.
Corollary promote' {t t' : T} : Preprocessed t -> Preprocessing t t' -> Preprocessing t (i t').
intros pre ed. apply (ipromote ed); try assumption; try apply drefl.
Qed.
Corollary promote {t t' : T} : Preprocessing (i t) t' -> Preprocessing (i t) (i t').
apply promote'. apply i_preprocessed.
Qed.
Corollary map {t t' : T} : Preprocessing t t' -> Preprocessing (i t) (i t').
intro ed. apply promote. apply derelict. assumption.
Qed.
End Comonad.
Section Transitivity.
Import Decidable.Reduction.
Theorem decidable_transPV' {tc tc' : T} {bcon : Con tc tc'} (bind : forall req : Req bcon, Preprocessing (Ass req left) (Ass req right)) {v : Variance} {t1 t2 t3 t4 : T} : Preprocessed t1 -> Decidable t1 t2 -> DecidablePV (Requires bcon) v t2 t3 -> Decidable t3 t4 -> Preprocessing t1 t4.
revert v t1 t4. apply (fun R rec => d_trace_ind R rec t2 t3). clear t2 t3. intros t2 t3 rec v t1 t4 it1 d ed d'. induction ed as [ v t2 t3 req | v t2 t3 mcon mass mrec ].
destruct req as [ req ]. apply (fun d => decidable_trans it1 d (bind req) d'). unfold Ass. destruct (Opt req) as [ _ | ]; try apply dpromote'; assumption.
pose proof (rec mcon) as rec. destruct d as [ t1 t2 lcon lass ]. pose proof (DRule.Red lcon mcon) as lmact. destruct lmact as [ mreq mvar lmact e | lmcon lmact ].
pose proof (mrec mreq) as mrec. apply mrec.
intros mcon' mreq' t2' t3' trace. apply rec with mreq. revert trace. apply Decidable.Proof.trace_comp'. apply Decidable.Proof.recursion with mcon' mreq'. apply Decidable.Proof.assumption.
apply (@decidablePV_decidable covariant). revert lmact. apply dbindV. clear v mass. intros v t t' lreq. destruct lreq as [ lreq ]. apply decidable_decidablePV. apply lass.
rewrite e. assumption.
clear mrec. assert (forall (v : Variance) (t2 t3 : T) (mreq : Requires mcon v t2 t3) (t1 t4 : T), Preprocessed t1 -> Decidable t1 t2 -> Decidable t3 t4 -> Preprocessing t1 t4) as rec'.
clear lass d' lmcon lmact t1 t4 lcon it1. intros v' t2' t3' mreq t1 t4 it1 d d'. destruct mreq as [ mreq ]. eapply rec; try assumption.
apply Decidable.Proof.assumption.
exact d.
apply mass.
assumption.
clear rec. rename rec' into rec. destruct d' as [ t3 t4 rcon rass ]. pose proof (Decidable.Red' lmcon rcon) as act. apply decidableP_preprocessing; try assumption. clear it1. assert (forall (v : Variance) (t3' t4' : T), Requires rcon v t3' t4' -> Decidable t3' t4') as rass'.
intros v' t3' t4' rreq. destruct rreq as [ rreq ]. apply rass.
clear rass. rename rass' into rass. assert (forall (v : Variance) (t1' t2' : T), Requires lcon v t1' t2' -> Decidable t1' t2') as lass'.
intros v' t1' t2' lreq. destruct lreq as [ lreq ]. apply lass.
clear lass. rename lass' into lass. assert (forall (v : Variance) (t2 t4 : T), Requires lmcon v t2 t4 -> DecidablePV (fun _ t2 t3 => forall t1 t4 : T, Preprocessed t1 -> Decidable t1 t2 -> Decidable t3 t4 -> Preprocessing t1 t4) v t2 t4) as lmact'.
intros v' t2' t3' lmreq. destruct lmreq as [ lmreq ]. generalize (lmact lmreq). apply dbindV. clear lmact lmreq rass rcon act lmcon. intros v' t2' t4' comp. apply trans_decidel in comp; try assumption. clear lass lcon. revert comp. apply dmonoV. clear v' t2' t4'. intros v' t2' t4' coma. destruct v'; [ destruct coma as [ t3' d mreq ] | destruct coma as [ t3' mreq d' ] ]; pose proof (rec _ _ _ mreq) as rec; clear mreq; intros t1' t5' it1' d1 d5; apply rec; try assumption.
revert d1 d. apply dtrans.
revert d' d5. apply dtrans.
clear lmact mass rec lcon mcon lass t2. rename lmact' into lmact. apply (@decidablePV_decidableP covariant). revert act. apply dbindV. intros v' t1' t4' comp. apply trans_decider in comp; try assumption. clear rass rcon. revert comp. apply dbindV. clear v' t1' t4'. intros v' t1' t4' coma. destruct v'; [ destruct coma as [ t3' lmreq d' ] | destruct coma as [ t2' d lmreq ] ]; pose proof (lmact _ _ _ lmreq) as lmact; clear lmreq lmcon t1 t3 t4.
apply (decidable_decidablePV covariant) in d'. generalize (Decidable.transPV lmact d'). clear lmact t3' d'. apply dbindV. clear t1' t4'. intros v' t1 t4 trans. apply trans_decider in trans; [ | intros t t' v'' f; destruct f ]. revert trans. apply dmonoV. clear v' t1 t4. intros v' t1 t4 coma t0 t5 it0 d0 d5. destruct v'; [ destruct coma as [ t3 trans d ] | destruct coma as [ t3 d trans ] ]; apply trans; try assumption.
revert d d5. apply dtrans.
revert d0 d. apply dtrans.
apply (decidable_decidablePV contravariant) in d. generalize (Decidable.trans_contra d lmact). clear d lmact t2'. apply dbindV. clear t1' t4'. intros v' t1 t4 trans. apply trans_decider in trans; [ | intros t t' v'' f; destruct f ]. revert trans. apply dmonoV. clear v' t1 t4. intros v' t1 t4 coma t0 t5 it0 d0 d5. destruct v'; [ destruct coma as [ t3 trans d ] | destruct coma as [ t3 d trans ] ]; apply trans; try assumption.
revert d d5. apply dtrans.
revert d0 d. apply dtrans.
Qed.
Lemma decidable_ipreprocessingPV' {t1 t2 : T} {con : Con t1 t2} (bind : forall req : Req con, Preprocessing (Ass req left) (Ass req right)) {v : Variance} {t t' : T} : DecidablePV (Requires con) v t t' -> Preprocessing (i t) t'.
intro d. eapply decidable_transPV'.
exact bind.
apply i_preprocessed.
apply counit.
exact d.
apply drefl.
Qed.
Lemma decidable_preprocessingPV (P : Variance -> T -> T -> Prop) (v : Variance) (t t' : T) : (forall (v : Variance) (t1 t2 t3 t4 : T), Decidable t1 t2 -> P v t2 t3 -> Decidable t3 t4 -> P v t1 t4) -> DecidablePV P v t t' -> ProofPV P v t t'.
intro transd. revert v. apply (fun R rec => i_wf R rec t t'). clear t t'. intros t t' rec v d. destruct d as [ v t t' p | v t t' con ass ].
apply permitV. assumption.
apply (proofPV _ con). intro req. apply rec. simpl. pose proof (ass req) as ass. unfold Var. destruct (multiply v (ORule.Var req)).
revert ass. apply @Decidable.transPV' with (fun v t t' => False).
clear v con req rec t t'. intros v t t' trans. destruct trans as [ coma | coma ].
destruct v; [ destruct coma as [ t2 f d ] | destruct coma as [ t2 d f ] ]; destruct f.
destruct v; [ destruct coma as [ t2 d p ] | destruct coma as [ t2 p d ] ]; apply decidablePV_decidable in d.
apply transd with t2 t'; try assumption. apply drefl.
apply transd with t t2; try assumption. apply drefl.
apply decidable_decidablePV. destruct (Opt req) as [ _ | ]; [ apply drefl | apply counit ].
revert ass. apply @Decidable.trans_contra' with (fun v t t' => False).
clear v con req rec t t'. intros v t t' trans. destruct trans as [ coma | coma ].
destruct v; [ destruct coma as [ t2 p d ] | destruct coma as [ t2 d p ] ]; apply decidablePV_decidable in d.
apply transd with t t2; try assumption. apply drefl.
apply transd with t2 t'; try assumption. apply drefl.
destruct v; [ destruct coma as [ t2 d f ] | destruct coma as [ t2 f d ] ]; destruct f.
apply decidable_decidablePV. destruct (Opt req) as [ _ | ]; [ apply drefl | apply counit ].
Qed.
Lemma decidable_preprocessingPV' (P : Variance -> T -> T -> Prop) (v : Variance) (t t' : T) : DecidablePV P v t t' -> ProofPV (Comaposition (fun v => Decidable) (Comaposition P (fun v => Decidable))) v t t'.
intro d. apply decidable_preprocessingPV.
clear v t t' d. intros v t1 t2 t5 t6 d coma d'''. destruct v; [ destruct coma as [ t3 d' comp ] | destruct coma as [ t4 contra d'' ] ].
apply compose with t3.
revert d d'. apply dtrans.
destruct comp as [ t4 p d'' ]. apply compose with t4; try assumption. revert d'' d'''. apply dtrans.
apply contrapose with t4.
destruct contra as [ t3 d' p ]. apply contrapose with t3; try assumption. revert d d'. apply dtrans.
revert d'' d'''. apply dtrans.
revert d. apply dmonoV. clear v t t'. intros v t t' p. destruct v.
apply compose with t; try apply drefl. apply compose with t'; try apply drefl. assumption.
apply contrapose with t'.
apply contrapose with t.
apply drefl.
assumption.
apply drefl.
Qed.
Lemma trans {t1 t2 t3 : T} : Preprocessed t1 -> Preprocessing t1 t2 -> Preprocessing t2 t3 -> Preprocessing t1 t3.
intros it1 ed ed'. generalize (drefl t3). revert ed ed'. generalize (drefl t1). revert it1. generalize t3 at 1 2 as t3'. revert t2. generalize t1 at 3 4 as t1'. apply (fun R rec => i_trace_ind R rec t1 t3). clear t1 t3. intros t1 t5 rec t2 t3 t4 it1 d ed ed' d'. simpl in rec. apply map in ed'. apply dderelict in d'. apply map in ed. apply (dpromote' it1) in d. generalize (decidable_trans (i_preprocessed _) (drefl _) ed' d'). clear ed' d'. intro ed'. generalize (decidable_trans it1 d ed (drefl _)). clear d ed. intro ed. clear t2 t4. revert ed ed'. generalize (i t3) as t3'. clear t3. intros t3 ed ed'. induction ed' as [ t3 t5 rcon rass rrec ]. destruct ed as [ t1 t2 lcon lass ]. pose proof (DRule.Red lcon rcon) as act. destruct act as [ rreq ev lact er | tcon act ].
pose proof (rrec rreq) as rrec. unfold Ass in rrec. rewrite er in rrec. clear er. apply rrec.
assumption.
clear rrec. destruct (Opt rreq) as [ _ | ].
apply (fun ed => decidable_trans it1 (dpreprocessed it1) ed (drefl _)). revert lact. apply decidable_ipreprocessingPV'. assumption.
apply promote'; try assumption. eapply decidable_transPV'; try exact lact; try assumption; apply drefl.
clear rrec. apply (proof tcon). intro treq. pose proof (act treq) as act. pose proof (rec tcon treq) as rec. assert (DecidablePV (Comaposition (DecidablePV (fun v t t' => False)) (Comaposition (Transitivity (Requires lcon) (Requires rcon)) (DecidablePV (fun v t t' => False)))) (Var treq) (Ass treq left) (Ass treq right)) as act'.
unfold Var. destruct (ORule.Var treq).
revert act. eapply Decidable.transPV'; [ | eapply (decidable_decidablePV covariant _ _ ) ].
intros v t1' t4' trans. destruct trans as [ coma | coma ]; [ destruct v; [ destruct coma as [ t2' f _ ] | destruct coma as [ t3' _ f ] ]; destruct f | ]. destruct v; [ destruct coma as [ t2' d trans ] | destruct coma as [ t3' trans d ] ].
apply compose with t2'; try assumption. apply compose with t4'; try assumption. apply decidable_decidablePV. apply drefl.
apply contrapose with t3'; try assumption. apply contrapose with t1'; try assumption. apply decidable_decidablePV. apply drefl.
unfold Ass. destruct (Opt treq) as [ _ | ].
apply drefl.
apply counit.
revert act. eapply Decidable.trans_contra'; [ | eapply (decidable_decidablePV contravariant _ _ ) ].
intros v t1' t4' trans. destruct trans as [ coma | coma ]; [ | destruct v; [ destruct coma as [ t2' _ f ] | destruct coma as [ t3' f _ ] ]; destruct f ]. destruct v; [ destruct coma as [ t3' trans d ] | destruct coma as [ t2' d trans ] ].
apply compose with t1'; try (apply decidable_decidablePV; apply drefl). apply compose with t3'; try assumption.
apply contrapose with t4'.
apply contrapose with t2'; try assumption.
apply decidable_decidablePV. apply drefl.
unfold Ass. destruct (Opt treq) as [ _ | ].
apply drefl.
apply counit.
clear act. rename act' into act. apply decidable_preprocessingPV' in act. assert (Preprocessed (Ass treq left)) as pre; [ unfold Ass; destruct (Opt treq) as [ preserve | ]; [ auto | apply i_preprocessed ] | ]. clear it1. revert pre. fold (Ass treq left) in rec. fold (Ass treq right) in rec. revert rec act. generalize (Ass treq right) as t5'. generalize (Ass treq left) as t1'. generalize (Var treq) as v. clear tcon treq. intros v t1' t5' rec act it1'. induction act as [ v t1' t5' coma | v t1' t5' tcon tass trec ].
assert (exists2 t2' : T, Decidable t1' t2' & exists2 t4' : T, Transitivity (Requires lcon) (Requires rcon) v t2' t4' & Decidable t4' t5') as comp.
destruct v; [ destruct coma as [ t2' d comp ] | destruct coma as [ t4' contra d' ] ].
destruct comp as [ t4' comp d' ]. destruct comp as [ t3' d1 comp ]. apply decidablePV_decidable in d1. destruct comp as [ t comp d1' ]. apply decidablePV_decidable in d1'. apply ex_intro2 with t3'.
revert d d1. apply dtrans.
apply ex_intro2 with t; try assumption. revert d1' d'. apply dtrans.
destruct contra as [ t2' d contra ]. destruct contra as [ t3' contra d1' ]. destruct contra as [ t d1 comp ]. apply ex_intro2 with t.
apply decidablePV_decidable in d1. revert d d1. apply dtrans.
apply ex_intro2 with t3'; try assumption. apply decidablePV_decidable in d1'. revert d1' d'. apply dtrans.
clear coma. destruct comp as [ t2' d [ t4' trans d' ] ]. pose proof (fun t3' ed ed' => rec t1' t5' (assumption t1' t5') (i t2') t3' t4' it1' (dtrans (dpreprocessed it1') (dmap d)) ed ed' d') as rec. clear it1' d d'. destruct trans as [ coma | coma ].
destruct v; [ destruct coma as [ t3' lreq rreq ] | destruct coma as [ t3' rreq lreq ] ].
apply rec with (i t3').
destruct lreq as [ lreq ]. apply promote. pose proof (lass lreq) as lass. unfold Ass in lass. destruct (Opt lreq) as [ _ | ]; [ apply derelict | ]; assumption.
revert rreq. apply decidable_ipreprocessingPV'. assumption.
apply rec with (i t3').
apply promote. revert rreq. apply decidable_ipreprocessingPV'. assumption.
destruct lreq as [ lreq ]. pose proof (lass lreq) as lass. unfold Ass in lass. destruct (Opt lreq) as [ _ | ]; [ apply derelict | ]; assumption.
destruct v; [ destruct coma as [ t3' lreq rreq ] | destruct coma as [ t3' rreq lreq ] ].
apply rec with (i t3').
apply promote. revert lreq. apply decidable_ipreprocessingPV'. assumption.
destruct rreq as [ rreq ]. pose proof (rass rreq) as rass. unfold Ass in rass. destruct (Opt rreq) as [ _ | ]; [ apply derelict | ]; assumption.
apply rec with (i t3').
destruct rreq as [ rreq ]. apply promote. pose proof (rass rreq) as rass. unfold Ass in rass. destruct (Opt rreq) as [ _ | ]; [ apply derelict | ]; assumption.
revert lreq. apply decidable_ipreprocessingPV'. assumption.
simpl in trec. apply (proof tcon). intro treq. apply trec.
intros t t' trace. apply rec. revert trace. apply trace_comp'. apply recursion with tcon treq. apply assumption.
destruct (Opt treq) as [ preserve | ].
apply preserve. assumption.
apply i_preprocessed.
Qed.
Corollary itrans {t1 t2 t3 : T} : iPreprocessing t1 t2 -> iPreprocessing t2 t3 -> iPreprocessing t1 t3.
intros ed ed' t0 t4 pre d d'. apply @trans with (i t2); try assumption.
apply promote'; try assumption. apply ed; try assumption. apply drefl.
apply ed'; try assumption.
apply i_preprocessed.
apply counit.
Qed.
End Transitivity.
Section Decider.
Theorem decider' (t t' : T) : Preprocessed t -> { Preprocessing t t' } + { Preprocessing t t' -> False }.
apply (fun R rec => i_wf R rec t t'). clear t t'. intros t t' rec pre. destruct (DRule.finite_con t t') as [ lcon finite_req finite ]. assert ({ Preprocessing t t' } + { Forall (fun con : Con t t' => exists req : Req con, Preprocessing (Ass req left) (Ass req right) -> False) lcon }) as inv.
clear finite. induction finite_req as [ | con lcon lreq finite_req ind ]; [ right; apply Forall_nil | ]. destruct ind as [ ind | ind ]; [ left; assumption | ]. destruct lreq as [ lreq finite ]. assert ({ Forall (fun req : Req con => Preprocessing (Ass req left) (Ass req right)) lreq } + { exists req : Req con, Preprocessing (Ass req left) (Ass req right) -> False }) as inv.
clear finite. induction lreq as [ | req lreq rreq ]; [ left; apply Forall_nil | ]. destruct rreq as [ rreq | rreq ]; [ | right; assumption ]. pose proof (rec con req) as rec. destruct rec as [ rec | rec ].
unfold WFI.PRule.Ass. destruct (Opt req) as [ preserve | ].
apply preserve. assumption.
apply i_preprocessed.
left. apply Forall_cons; assumption.
right. apply ex_intro with req. assumption.
destruct inv as [ inv | inv ].
left. apply proof with con. intro req. apply (fun inv => proj1 (Forall_forall _ lreq) inv req) in inv; try assumption. apply finite.
right. apply Forall_cons; assumption.
clear finite_req. destruct inv as [ inv | inv ]; [ left; assumption | ]. right. intro d. assert (Exists (fun con' : Rule.Con t t' => forall req' : Rule.Req con', iPreprocessing (Rule.Ass req' left) (Rule.Ass req' right)) lcon) as fin.
destruct d as [ t t' con ass ]. apply finite with con.
exact iadmitsd.
clear pre. intros t1 t2 t3 t4 d ed d' t0 t5 pre d0 d5. apply ed; try assumption.
revert d0 d. apply dtrans.
revert d' d5. apply dtrans.
intros req t1 t4 pre' d d'. pose proof (ass req) as ass. unfold Ass in ass. destruct (Opt req) as [ preserve | ].
revert d ass d'. apply decidable_trans. assumption.
apply dpromote' in d; try assumption. revert d ass d'. apply decidable_trans. assumption.
clear d finite. induction fin as [ con' lcon d | con' lcon fin ind ].
apply Forall_inv in inv. destruct inv as [ req' nd ]. apply nd. pose proof (d req') as d. apply d.
unfold Ass. destruct (Opt req') as [ preserve | ].
apply preserve. assumption.
apply i_preprocessed.
unfold Ass. destruct (Opt req') as [ _ | ].
apply drefl.
apply counit.
apply drefl.
apply ind. inversion inv. assumption.
Qed.
Corollary decider (t t' : T) : { Preprocessing (i t) t' } + { Preprocessing (i t) t' -> False }.
apply decider'. apply i_preprocessed.
Qed.
End Decider.
End Preprocessing.
Require Import Decide.
Require Import Coq.Lists.List.
Module Type Comonad (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule).
Import T.
Import Rule.
Module Decidable := Decidable T Rule ORule DRule.
Import Decidable.
Parameter i : T -> T.
Parameter counit : forall t : T, Decidable (i t) t.
Parameter Preprocessed : T -> Prop.
Parameter i_preprocessed : forall t : T, Preprocessed (i t).
Parameter Opt : forall {t t' : T} {con : Con t t'} (req : Req con), option (Preprocessed t -> Preprocessed (Ass req left)).
Parameter i_promote_R : forall R : T -> T -> Prop, (forall t, R t t) -> (forall t1 t2 t3 t4 : T, Decidable t1 t2 -> R t2 t3 -> Decidable t3 t4 -> R t1 t4) -> AdmitsD R -> Decidable.Proof.Inverts Preprocessed R -> forall (t t' : T) (con : Con t t'), Preprocessed t -> (forall req : Req con, R (Rule.Ass req left) (Rule.Ass req right)) -> (forall req : Req con, Preprocessed (Ass req left) -> R (Ass req left) (i (Ass req right))) -> R t (i t').
End Comonad.
Module PreprocessingRules (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule) (I : Comonad T Rule ORule DRule) <: Rules T.
Import T.
Import I.
Definition Con := Rule.Con.
Definition Req : forall {t t' : T}, Con t t' -> Type
:= @Rule.Req.
Definition Ass : forall {t t' : T} {con : Con t t'}, Req con -> Position -> T
:= fun t t' con req pos => match pos with
| left => match Opt req with
| None => i (Rule.Ass req left)
| Some _ => Rule.Ass req left
end
| right => Rule.Ass req right
end.
Definition Var : forall {t t' : T} {con : Con t t'}, Req con -> Variance := @ORule.Var.
End PreprocessingRules.
Module Type WellFoundedComonad (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule) (I : Comonad T Rule ORule DRule).
Import T.
Import Rule.
Import I.
Module PRule := PreprocessingRules T Rule ORule DRule I.
Import PRule.
Parameter i_wf : forall (R : T -> T -> Type), (forall t1 t2 : T, (forall (con : Con t1 t2) (req : Req con), R (Ass req left) (Ass req right)) -> R t1 t2) -> forall t t' : T, R t t'.
End WellFoundedComonad.
Module Preprocessing (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule) (I : Comonad T Rule ORule DRule) (WFI : WellFoundedComonad T Rule ORule DRule I).
Import T.
Import I.
Import WFI.
Module PRule := WFI.PRule.
Import PRule.
Module ProofPV := ProofPV T PRule PRule.
Import ProofPV.
Module Proof := ProofPV.Proof.
Import Proof.
Module Decidable := I.Decidable.
Import Decidable.
Definition Preprocessing := Proof.
Section PreprocessingDecidable.
Local Definition drefl := DRule.refl.
Local Definition dtrans : forall {t1 t2 t3 : T}, Decidable t1 t2 -> Decidable t2 t3 -> Decidable t1 t3 := @Decidable.trans.
Lemma dderelict {t t' : T} : Decidable t t' -> Decidable (i t) t'.
apply dtrans. apply counit.
Qed.
Lemma dpromote' {t t' : T} : Preprocessed t -> Decidable t t' -> Decidable t (i t').
intros pre d. revert pre. induction d as [ t t' con ass rec ]. intro pre. apply i_promote_R with con; try clear t t' con ass rec pre.
exact DRule.refl.
intros t1 t2 t3 t4 d d'. apply dtrans. revert d d'. apply dtrans.
apply Decidable.Proof.proof_admits.
intros t t' pre d. induction d as [ t t' con ass rec ]. apply Decidable.Proof.inversion with con; assumption.
assumption.
assumption.
assumption.
Qed.
Corollary dpromote {t t' : T} : Decidable (i t) t' -> Decidable (i t) (i t').
apply dpromote'. apply i_preprocessed.
Qed.
Corollary dpreprocessed {t : T} : Preprocessed t -> Decidable t (i t).
intro pre. apply dpromote'; try assumption. apply drefl.
Qed.
Corollary dmap {t t' : T} : Decidable t t' -> Decidable (i t) (i t').
intro d. apply dpromote. apply dderelict. assumption.
Qed.
End PreprocessingDecidable.
Section PreprocessingDecidableTrans.
Local Definition DecidableP := Decidable.Proof.ProofP.
Local Definition DecidablePV := Decidable.ProofPV.ProofPV.
Local Definition dpermitV := Decidable.ProofPV.permitV.
Local Definition dmonoV := @Decidable.ProofPV.monoV.
Local Definition dbindV := @Decidable.ProofPV.bindV.
Local Definition decidable_decidablePV := Decidable.ProofPV.proof_proofPV.
Local Definition decidablePV_decidable := @Decidable.ProofPV.proofPV_proof.
Local Definition decidableP_decidablePV := @Decidable.ProofPV.proofP_proofPV.
Local Definition decidablePV_decidableP := @Decidable.ProofPV.proofPV_proofP.
Import Decidable.Reduction.
Lemma decidableP_preprocessing {t1 t4 : T} : Preprocessed t1 -> DecidableP (fun t2 t3 => forall t1 t4 : T, Preprocessed t1 -> Decidable t1 t2 -> Decidable t3 t4 -> Preprocessing t1 t4) t1 t4 -> Preprocessing t1 t4.
apply (fun R rec => i_wf R rec t1 t4). clear t1 t4. intros t1 t4 rec id1 progress. simpl in rec. revert progress. generalize covariant. intros v progress. destruct progress as [ t1 t4 trans | t1 t4 con ass ].
apply trans; try trivial; try apply drefl.
apply (proof con). fold Preprocessing. intro req. apply rec.
destruct (Opt req) as [ preserve | ].
apply preserve. assumption.
apply i_preprocessed.
pose proof (ass req) as progress. clear ass rec id1 v. destruct (Opt req) as [ _ | ]; try assumption. apply (@decidablePV_decidableP covariant). pose proof (counit (Rule.Ass req left)) as d. apply (decidable_decidablePV covariant) in d. apply (decidableP_decidablePV covariant) in progress. generalize (Decidable.transPV d progress). clear d progress. apply dbindV. clear t1 t4 con req. intros v t1 t4 trans. apply trans_decidel in trans; [ | intros v' t t' f; destruct f ]. revert trans. apply dmonoV. clear v t1 t4. intros v t2 t3 coma t1 t4 it1 d1 d4. destruct v; [ destruct coma as [ t d trans ] | destruct coma as [ t trans d' ] ].
apply trans; try trivial. revert d1 d. apply dtrans.
apply trans; try trivial. revert d' d4. apply dtrans.
Qed.
Theorem decidable_trans {t1 t2 t3 t4 : T} : Preprocessed t1 -> Decidable t1 t2 -> Preprocessing t2 t3 -> Decidable t3 t4 -> Preprocessing t1 t4.
revert t1 t4. apply (fun R rec => i_trace_ind R rec t2 t3). clear t2 t3. intros t2 t3 rec t1 t4 it1 d ed d'. induction ed as [ t2 t3 mcon mass mrec ]. fold Preprocessing in mass. pose proof (rec mcon) as rec. destruct d as [ t1 t2 lcon lass ]. pose proof (DRule.Red lcon mcon) as lmact. destruct lmact as [ mreq mvar lmact e | lmcon lmact ].
pose proof (mrec mreq) as mrec. apply mrec.
intros mcon' mreq' t2' t3' trace. apply rec with mreq. revert trace. apply trace_comp'. apply recursion with mcon' mreq'. apply assumption.
unfold Ass. destruct (Opt mreq) as [ _ | ].
apply (@decidablePV_decidable covariant). revert lmact. apply dbindV. intros v t t' lreq. destruct lreq as [ lreq ]. apply decidable_decidablePV. apply lass.
apply dpromote'; try assumption. apply (@decidablePV_decidable covariant). revert lmact. apply dbindV. intros v t t' lreq. destruct lreq as [ lreq ]. apply decidable_decidablePV. apply lass.
unfold Ass. rewrite e. assumption.
clear mrec. assert (forall (v : Variance) (t2 t3 : T) (mreq : Requires mcon v t2 t3) (t1 t4 : T), Preprocessed t1 -> Decidable t1 t2 -> Decidable t3 t4 -> Preprocessing t1 t4) as rec'.
clear lass d' lmcon lmact t1 t4 lcon it1. intros v t2' t3' mreq t1 t4 it1 d d'. destruct mreq as [ mreq ]. apply rec with mreq (Ass mreq left) (Ass mreq right); try assumption.
apply assumption.
unfold Ass. destruct (Opt mreq) as [ _ | ]; try apply dpromote'; assumption.
apply mass.
clear rec. rename rec' into rec. destruct d' as [ t3 t4 rcon rass ]. pose proof (Decidable.Red' lmcon rcon) as act. apply decidableP_preprocessing; try assumption. clear it1. assert (forall (v : Variance) (t3' t4' : T), Requires rcon v t3' t4' -> Decidable t3' t4') as rass'.
intros v t3' t4' rreq. destruct rreq as [ rreq ]. apply rass.
clear rass. rename rass' into rass. assert (forall (v : Variance) (t1' t2' : T), Requires lcon v t1' t2' -> Decidable t1' t2') as lass'.
intros v t1' t2' lreq. destruct lreq as [ lreq ]. apply lass.
clear lass. rename lass' into lass. assert (forall (v : Variance) (t2 t4 : T), Requires lmcon v t2 t4 -> DecidablePV (fun _ t2 t3 => forall t1 t4 : T, Preprocessed t1 -> Decidable t1 t2 -> Decidable t3 t4 -> Preprocessing t1 t4) v t2 t4) as lmact'.
intros v t2' t3' lmreq. destruct lmreq as [ lmreq ]. generalize (lmact lmreq). apply dbindV. clear lmact lmreq rass rcon act lmcon. intros v t2' t4' comp. apply trans_decidel in comp; try assumption. clear lass lcon. revert comp. apply dmonoV. clear v t2' t4'. intros v t2' t4' coma. destruct v; [ destruct coma as [ t3' d mreq ] | destruct coma as [ t3' mreq d' ] ]; pose proof (rec _ _ _ mreq) as rec; clear mreq; intros t1' t5' it1' d1 d5; apply rec; try assumption.
revert d1 d. apply dtrans.
revert d' d5. apply dtrans.
clear lmact mass rec lcon mcon lass t2. rename lmact' into lmact. apply (@decidablePV_decidableP covariant). revert act. apply dbindV. intros v t1' t4' comp. apply trans_decider in comp; try assumption. clear rass rcon. revert comp. apply dbindV. clear v t1' t4'. intros v t1' t4' coma. destruct v; [ destruct coma as [ t3' lmreq d' ] | destruct coma as [ t2' d lmreq ] ]; pose proof (lmact _ _ _ lmreq) as lmact; clear lmreq lmcon t1 t3 t4.
apply (decidable_decidablePV covariant) in d'. generalize (Decidable.transPV lmact d'). clear lmact t3' d'. apply dbindV. clear t1' t4'. intros v t1 t4 trans. apply trans_decider in trans; [ | intros t t' v' f; destruct f ]. revert trans. apply dmonoV. clear v t1 t4. intros v t1 t4 coma t0 t5 it0 d0 d5. destruct v; [ destruct coma as [ t3 trans d ] | destruct coma as [ t3 d trans ] ]; apply trans; try assumption.
revert d d5. apply dtrans.
revert d0 d. apply dtrans.
apply (decidable_decidablePV contravariant) in d. generalize (Decidable.trans_contra d lmact). clear d lmact t2'. apply dbindV. clear t1' t4'. intros v t1 t4 trans. apply trans_decider in trans; [ | intros t t' v' f; destruct f ]. revert trans. apply dmonoV. clear v t1 t4. intros v t1 t4 coma t0 t5 it0 d0 d5. destruct v; [ destruct coma as [ t3 trans d ] | destruct coma as [ t3 d trans ] ]; apply trans; try assumption.
revert d d5. apply dtrans.
revert d0 d. apply dtrans.
Qed.
End PreprocessingDecidableTrans.
Section Comonad.
Lemma derelict {t t' : T} : Preprocessing t t' -> Preprocessing (i t) t'.
intro ed. apply @decidable_trans with t t'.
apply i_preprocessed.
apply counit.
assumption.
apply DRule.refl.
Qed.
Lemma admitsd : AdmitsD Preprocessing.
intros t1 t2 con ass. apply (proof con). intro req. unfold Ass. destruct (Opt req) as [ _ | ].
apply ass.
apply derelict. apply ass.
Qed.
Definition iPreprocessing (t2 t3 : T) := forall t1 t4 : T, Preprocessed t1 -> Decidable t1 t2 -> Decidable t3 t4 -> Preprocessing t1 t4.
Lemma iadmitsd : AdmitsD iPreprocessing.
intros t2 t3 con ass t1 t4 pre d d'. apply decidableP_preprocessing; try assumption. clear pre. assert (DecidableP iPreprocessing t2 t4) as dp. assert (DecidableP iPreprocessing t2 t3) as ed; [ apply @Decidable.Proof.proofP with con; intro req; apply Decidable.Proof.permit; apply ass | clear con ass ]. apply Decidable.Proof.proof_proofP in d'. revert ed d'. apply Decidable.trans_bind. clear t1 t2 t3 t4 d. intros v t1 t3 trans. apply Decidable.Proof.permit. destruct trans as [ coma | coma ].
destruct v; [ destruct coma as [ t2 l r ] | destruct coma as [ t2 l r ] ].
apply Decidable.ProofPV.proofPV_proof in r. intros t0 t5 pre d d'. apply l; try assumption. revert r d'. apply Decidable.trans.
apply Decidable.ProofPV.proofPV_proof in l. intros t0 t5 pre d d'. apply r; try assumption. revert d l. apply Decidable.trans.
destruct v; [ destruct coma as [ t2 l r ] | destruct coma as [ t2 l r ] ].
destruct r.
destruct l.
clear d' t3 con ass. apply Decidable.Proof.proof_proofP in d. revert d dp. apply Decidable.trans_bind. clear t2 t1 t4. intros v t1 t3 trans. apply Decidable.Proof.permit. destruct trans as [ coma | coma ].
destruct v; [ destruct coma as [ t2 l r ] | destruct coma as [ t2 l r ] ].
destruct l.
destruct r.
destruct v; [ destruct coma as [ t2 l r ] | destruct coma as [ t2 l r ] ].
apply Decidable.ProofPV.proofPV_proof in l. intros t0 t5 pre d d'. apply r; try assumption. revert d l. apply Decidable.trans.
apply Decidable.ProofPV.proofPV_proof in r. intros t0 t5 pre d d'. apply l; try assumption. revert r d'. apply Decidable.trans.
Qed.
Lemma decidable_preprocessing {t t' : T} : Decidable t t' -> Preprocessing t t'.
intro d. induction d as [ t t' con _ rec ]. apply (proof con). intro req. unfold Ass. destruct (Opt req) as [ _ | ]; try apply derelict; apply rec.
Qed.
Lemma refl (t : T) : Preprocessing t t.
apply decidable_preprocessing. apply DRule.refl.
Qed.
Lemma iiinverts : Decidable.Proof.Inverts Preprocessed iPreprocessing.
intros t t'. apply (fun R rec => DRule.wf R rec t t'). clear t t'. intros t1 t2 rec pre ed. pose proof (ed t1 t2 pre (drefl _) (drefl _)) as ed. clear pre. destruct ed as [ t2 t3 con ass ]. apply Decidable.Proof.inversion with con.
intros req t1 t4 pre d d'. pose proof (ass req) as ass. unfold Ass in ass. destruct (Opt req) as [ _ | ].
revert pre d ass d'. apply @decidable_trans.
apply dpromote' in d; try assumption. revert pre d ass d'. apply @decidable_trans.
intros req pre. apply rec; try assumption. clear pre. intros t1 t4 pre d d'. pose proof (ass req) as ass. unfold Ass in ass. destruct (Opt req) as [ _ | ].
revert pre d ass d'. apply @decidable_trans.
apply dpromote' in d; try assumption. revert pre d ass d'. apply @decidable_trans.
Qed.
Lemma ipromote {t2 t3 : T} : Preprocessing t2 t3 -> Preprocessed t2 -> iPreprocessing t2 (i t3).
intro ed. induction ed as [ t2 t3 con ass rec ]. intro pre. apply (i_promote_R iPreprocessing) with con; try clear t2 t3 con ass rec pre.
intros t2 t1 t3 pre d d'. apply decidable_preprocessing. revert d d'. apply Decidable.trans.
intros t1 t2 t3 t4 d ed d' t t' pre' d'' d'''. apply ed; try assumption.
revert d'' d. apply dtrans.
revert d' d'''. apply dtrans.
exact iadmitsd.
exact iiinverts.
assumption.
intros req t1 t4 pre' d d'. pose proof (ass req) as ass. revert ass d'. apply decidable_trans; try assumption. unfold Ass. destruct (Opt req) as [ _ | ]; try apply dpromote'; assumption.
clear ass pre. intros req pre t1 t4 pre' d d'. apply rec with req; try assumption.
unfold Ass. destruct (Opt req) as [ _ | ]; try assumption. apply i_preprocessed.
unfold Ass. destruct (Opt req) as [ _ | ]; try assumption. apply dpromote'; assumption.
Qed.
Corollary promote' {t t' : T} : Preprocessed t -> Preprocessing t t' -> Preprocessing t (i t').
intros pre ed. apply (ipromote ed); try assumption; try apply drefl.
Qed.
Corollary promote {t t' : T} : Preprocessing (i t) t' -> Preprocessing (i t) (i t').
apply promote'. apply i_preprocessed.
Qed.
Corollary map {t t' : T} : Preprocessing t t' -> Preprocessing (i t) (i t').
intro ed. apply promote. apply derelict. assumption.
Qed.
End Comonad.
Section Transitivity.
Import Decidable.Reduction.
Theorem decidable_transPV' {tc tc' : T} {bcon : Con tc tc'} (bind : forall req : Req bcon, Preprocessing (Ass req left) (Ass req right)) {v : Variance} {t1 t2 t3 t4 : T} : Preprocessed t1 -> Decidable t1 t2 -> DecidablePV (Requires bcon) v t2 t3 -> Decidable t3 t4 -> Preprocessing t1 t4.
revert v t1 t4. apply (fun R rec => d_trace_ind R rec t2 t3). clear t2 t3. intros t2 t3 rec v t1 t4 it1 d ed d'. induction ed as [ v t2 t3 req | v t2 t3 mcon mass mrec ].
destruct req as [ req ]. apply (fun d => decidable_trans it1 d (bind req) d'). unfold Ass. destruct (Opt req) as [ _ | ]; try apply dpromote'; assumption.
pose proof (rec mcon) as rec. destruct d as [ t1 t2 lcon lass ]. pose proof (DRule.Red lcon mcon) as lmact. destruct lmact as [ mreq mvar lmact e | lmcon lmact ].
pose proof (mrec mreq) as mrec. apply mrec.
intros mcon' mreq' t2' t3' trace. apply rec with mreq. revert trace. apply Decidable.Proof.trace_comp'. apply Decidable.Proof.recursion with mcon' mreq'. apply Decidable.Proof.assumption.
apply (@decidablePV_decidable covariant). revert lmact. apply dbindV. clear v mass. intros v t t' lreq. destruct lreq as [ lreq ]. apply decidable_decidablePV. apply lass.
rewrite e. assumption.
clear mrec. assert (forall (v : Variance) (t2 t3 : T) (mreq : Requires mcon v t2 t3) (t1 t4 : T), Preprocessed t1 -> Decidable t1 t2 -> Decidable t3 t4 -> Preprocessing t1 t4) as rec'.
clear lass d' lmcon lmact t1 t4 lcon it1. intros v' t2' t3' mreq t1 t4 it1 d d'. destruct mreq as [ mreq ]. eapply rec; try assumption.
apply Decidable.Proof.assumption.
exact d.
apply mass.
assumption.
clear rec. rename rec' into rec. destruct d' as [ t3 t4 rcon rass ]. pose proof (Decidable.Red' lmcon rcon) as act. apply decidableP_preprocessing; try assumption. clear it1. assert (forall (v : Variance) (t3' t4' : T), Requires rcon v t3' t4' -> Decidable t3' t4') as rass'.
intros v' t3' t4' rreq. destruct rreq as [ rreq ]. apply rass.
clear rass. rename rass' into rass. assert (forall (v : Variance) (t1' t2' : T), Requires lcon v t1' t2' -> Decidable t1' t2') as lass'.
intros v' t1' t2' lreq. destruct lreq as [ lreq ]. apply lass.
clear lass. rename lass' into lass. assert (forall (v : Variance) (t2 t4 : T), Requires lmcon v t2 t4 -> DecidablePV (fun _ t2 t3 => forall t1 t4 : T, Preprocessed t1 -> Decidable t1 t2 -> Decidable t3 t4 -> Preprocessing t1 t4) v t2 t4) as lmact'.
intros v' t2' t3' lmreq. destruct lmreq as [ lmreq ]. generalize (lmact lmreq). apply dbindV. clear lmact lmreq rass rcon act lmcon. intros v' t2' t4' comp. apply trans_decidel in comp; try assumption. clear lass lcon. revert comp. apply dmonoV. clear v' t2' t4'. intros v' t2' t4' coma. destruct v'; [ destruct coma as [ t3' d mreq ] | destruct coma as [ t3' mreq d' ] ]; pose proof (rec _ _ _ mreq) as rec; clear mreq; intros t1' t5' it1' d1 d5; apply rec; try assumption.
revert d1 d. apply dtrans.
revert d' d5. apply dtrans.
clear lmact mass rec lcon mcon lass t2. rename lmact' into lmact. apply (@decidablePV_decidableP covariant). revert act. apply dbindV. intros v' t1' t4' comp. apply trans_decider in comp; try assumption. clear rass rcon. revert comp. apply dbindV. clear v' t1' t4'. intros v' t1' t4' coma. destruct v'; [ destruct coma as [ t3' lmreq d' ] | destruct coma as [ t2' d lmreq ] ]; pose proof (lmact _ _ _ lmreq) as lmact; clear lmreq lmcon t1 t3 t4.
apply (decidable_decidablePV covariant) in d'. generalize (Decidable.transPV lmact d'). clear lmact t3' d'. apply dbindV. clear t1' t4'. intros v' t1 t4 trans. apply trans_decider in trans; [ | intros t t' v'' f; destruct f ]. revert trans. apply dmonoV. clear v' t1 t4. intros v' t1 t4 coma t0 t5 it0 d0 d5. destruct v'; [ destruct coma as [ t3 trans d ] | destruct coma as [ t3 d trans ] ]; apply trans; try assumption.
revert d d5. apply dtrans.
revert d0 d. apply dtrans.
apply (decidable_decidablePV contravariant) in d. generalize (Decidable.trans_contra d lmact). clear d lmact t2'. apply dbindV. clear t1' t4'. intros v' t1 t4 trans. apply trans_decider in trans; [ | intros t t' v'' f; destruct f ]. revert trans. apply dmonoV. clear v' t1 t4. intros v' t1 t4 coma t0 t5 it0 d0 d5. destruct v'; [ destruct coma as [ t3 trans d ] | destruct coma as [ t3 d trans ] ]; apply trans; try assumption.
revert d d5. apply dtrans.
revert d0 d. apply dtrans.
Qed.
Lemma decidable_ipreprocessingPV' {t1 t2 : T} {con : Con t1 t2} (bind : forall req : Req con, Preprocessing (Ass req left) (Ass req right)) {v : Variance} {t t' : T} : DecidablePV (Requires con) v t t' -> Preprocessing (i t) t'.
intro d. eapply decidable_transPV'.
exact bind.
apply i_preprocessed.
apply counit.
exact d.
apply drefl.
Qed.
Lemma decidable_preprocessingPV (P : Variance -> T -> T -> Prop) (v : Variance) (t t' : T) : (forall (v : Variance) (t1 t2 t3 t4 : T), Decidable t1 t2 -> P v t2 t3 -> Decidable t3 t4 -> P v t1 t4) -> DecidablePV P v t t' -> ProofPV P v t t'.
intro transd. revert v. apply (fun R rec => i_wf R rec t t'). clear t t'. intros t t' rec v d. destruct d as [ v t t' p | v t t' con ass ].
apply permitV. assumption.
apply (proofPV _ con). intro req. apply rec. simpl. pose proof (ass req) as ass. unfold Var. destruct (multiply v (ORule.Var req)).
revert ass. apply @Decidable.transPV' with (fun v t t' => False).
clear v con req rec t t'. intros v t t' trans. destruct trans as [ coma | coma ].
destruct v; [ destruct coma as [ t2 f d ] | destruct coma as [ t2 d f ] ]; destruct f.
destruct v; [ destruct coma as [ t2 d p ] | destruct coma as [ t2 p d ] ]; apply decidablePV_decidable in d.
apply transd with t2 t'; try assumption. apply drefl.
apply transd with t t2; try assumption. apply drefl.
apply decidable_decidablePV. destruct (Opt req) as [ _ | ]; [ apply drefl | apply counit ].
revert ass. apply @Decidable.trans_contra' with (fun v t t' => False).
clear v con req rec t t'. intros v t t' trans. destruct trans as [ coma | coma ].
destruct v; [ destruct coma as [ t2 p d ] | destruct coma as [ t2 d p ] ]; apply decidablePV_decidable in d.
apply transd with t t2; try assumption. apply drefl.
apply transd with t2 t'; try assumption. apply drefl.
destruct v; [ destruct coma as [ t2 d f ] | destruct coma as [ t2 f d ] ]; destruct f.
apply decidable_decidablePV. destruct (Opt req) as [ _ | ]; [ apply drefl | apply counit ].
Qed.
Lemma decidable_preprocessingPV' (P : Variance -> T -> T -> Prop) (v : Variance) (t t' : T) : DecidablePV P v t t' -> ProofPV (Comaposition (fun v => Decidable) (Comaposition P (fun v => Decidable))) v t t'.
intro d. apply decidable_preprocessingPV.
clear v t t' d. intros v t1 t2 t5 t6 d coma d'''. destruct v; [ destruct coma as [ t3 d' comp ] | destruct coma as [ t4 contra d'' ] ].
apply compose with t3.
revert d d'. apply dtrans.
destruct comp as [ t4 p d'' ]. apply compose with t4; try assumption. revert d'' d'''. apply dtrans.
apply contrapose with t4.
destruct contra as [ t3 d' p ]. apply contrapose with t3; try assumption. revert d d'. apply dtrans.
revert d'' d'''. apply dtrans.
revert d. apply dmonoV. clear v t t'. intros v t t' p. destruct v.
apply compose with t; try apply drefl. apply compose with t'; try apply drefl. assumption.
apply contrapose with t'.
apply contrapose with t.
apply drefl.
assumption.
apply drefl.
Qed.
Lemma trans {t1 t2 t3 : T} : Preprocessed t1 -> Preprocessing t1 t2 -> Preprocessing t2 t3 -> Preprocessing t1 t3.
intros it1 ed ed'. generalize (drefl t3). revert ed ed'. generalize (drefl t1). revert it1. generalize t3 at 1 2 as t3'. revert t2. generalize t1 at 3 4 as t1'. apply (fun R rec => i_trace_ind R rec t1 t3). clear t1 t3. intros t1 t5 rec t2 t3 t4 it1 d ed ed' d'. simpl in rec. apply map in ed'. apply dderelict in d'. apply map in ed. apply (dpromote' it1) in d. generalize (decidable_trans (i_preprocessed _) (drefl _) ed' d'). clear ed' d'. intro ed'. generalize (decidable_trans it1 d ed (drefl _)). clear d ed. intro ed. clear t2 t4. revert ed ed'. generalize (i t3) as t3'. clear t3. intros t3 ed ed'. induction ed' as [ t3 t5 rcon rass rrec ]. destruct ed as [ t1 t2 lcon lass ]. pose proof (DRule.Red lcon rcon) as act. destruct act as [ rreq ev lact er | tcon act ].
pose proof (rrec rreq) as rrec. unfold Ass in rrec. rewrite er in rrec. clear er. apply rrec.
assumption.
clear rrec. destruct (Opt rreq) as [ _ | ].
apply (fun ed => decidable_trans it1 (dpreprocessed it1) ed (drefl _)). revert lact. apply decidable_ipreprocessingPV'. assumption.
apply promote'; try assumption. eapply decidable_transPV'; try exact lact; try assumption; apply drefl.
clear rrec. apply (proof tcon). intro treq. pose proof (act treq) as act. pose proof (rec tcon treq) as rec. assert (DecidablePV (Comaposition (DecidablePV (fun v t t' => False)) (Comaposition (Transitivity (Requires lcon) (Requires rcon)) (DecidablePV (fun v t t' => False)))) (Var treq) (Ass treq left) (Ass treq right)) as act'.
unfold Var. destruct (ORule.Var treq).
revert act. eapply Decidable.transPV'; [ | eapply (decidable_decidablePV covariant _ _ ) ].
intros v t1' t4' trans. destruct trans as [ coma | coma ]; [ destruct v; [ destruct coma as [ t2' f _ ] | destruct coma as [ t3' _ f ] ]; destruct f | ]. destruct v; [ destruct coma as [ t2' d trans ] | destruct coma as [ t3' trans d ] ].
apply compose with t2'; try assumption. apply compose with t4'; try assumption. apply decidable_decidablePV. apply drefl.
apply contrapose with t3'; try assumption. apply contrapose with t1'; try assumption. apply decidable_decidablePV. apply drefl.
unfold Ass. destruct (Opt treq) as [ _ | ].
apply drefl.
apply counit.
revert act. eapply Decidable.trans_contra'; [ | eapply (decidable_decidablePV contravariant _ _ ) ].
intros v t1' t4' trans. destruct trans as [ coma | coma ]; [ | destruct v; [ destruct coma as [ t2' _ f ] | destruct coma as [ t3' f _ ] ]; destruct f ]. destruct v; [ destruct coma as [ t3' trans d ] | destruct coma as [ t2' d trans ] ].
apply compose with t1'; try (apply decidable_decidablePV; apply drefl). apply compose with t3'; try assumption.
apply contrapose with t4'.
apply contrapose with t2'; try assumption.
apply decidable_decidablePV. apply drefl.
unfold Ass. destruct (Opt treq) as [ _ | ].
apply drefl.
apply counit.
clear act. rename act' into act. apply decidable_preprocessingPV' in act. assert (Preprocessed (Ass treq left)) as pre; [ unfold Ass; destruct (Opt treq) as [ preserve | ]; [ auto | apply i_preprocessed ] | ]. clear it1. revert pre. fold (Ass treq left) in rec. fold (Ass treq right) in rec. revert rec act. generalize (Ass treq right) as t5'. generalize (Ass treq left) as t1'. generalize (Var treq) as v. clear tcon treq. intros v t1' t5' rec act it1'. induction act as [ v t1' t5' coma | v t1' t5' tcon tass trec ].
assert (exists2 t2' : T, Decidable t1' t2' & exists2 t4' : T, Transitivity (Requires lcon) (Requires rcon) v t2' t4' & Decidable t4' t5') as comp.
destruct v; [ destruct coma as [ t2' d comp ] | destruct coma as [ t4' contra d' ] ].
destruct comp as [ t4' comp d' ]. destruct comp as [ t3' d1 comp ]. apply decidablePV_decidable in d1. destruct comp as [ t comp d1' ]. apply decidablePV_decidable in d1'. apply ex_intro2 with t3'.
revert d d1. apply dtrans.
apply ex_intro2 with t; try assumption. revert d1' d'. apply dtrans.
destruct contra as [ t2' d contra ]. destruct contra as [ t3' contra d1' ]. destruct contra as [ t d1 comp ]. apply ex_intro2 with t.
apply decidablePV_decidable in d1. revert d d1. apply dtrans.
apply ex_intro2 with t3'; try assumption. apply decidablePV_decidable in d1'. revert d1' d'. apply dtrans.
clear coma. destruct comp as [ t2' d [ t4' trans d' ] ]. pose proof (fun t3' ed ed' => rec t1' t5' (assumption t1' t5') (i t2') t3' t4' it1' (dtrans (dpreprocessed it1') (dmap d)) ed ed' d') as rec. clear it1' d d'. destruct trans as [ coma | coma ].
destruct v; [ destruct coma as [ t3' lreq rreq ] | destruct coma as [ t3' rreq lreq ] ].
apply rec with (i t3').
destruct lreq as [ lreq ]. apply promote. pose proof (lass lreq) as lass. unfold Ass in lass. destruct (Opt lreq) as [ _ | ]; [ apply derelict | ]; assumption.
revert rreq. apply decidable_ipreprocessingPV'. assumption.
apply rec with (i t3').
apply promote. revert rreq. apply decidable_ipreprocessingPV'. assumption.
destruct lreq as [ lreq ]. pose proof (lass lreq) as lass. unfold Ass in lass. destruct (Opt lreq) as [ _ | ]; [ apply derelict | ]; assumption.
destruct v; [ destruct coma as [ t3' lreq rreq ] | destruct coma as [ t3' rreq lreq ] ].
apply rec with (i t3').
apply promote. revert lreq. apply decidable_ipreprocessingPV'. assumption.
destruct rreq as [ rreq ]. pose proof (rass rreq) as rass. unfold Ass in rass. destruct (Opt rreq) as [ _ | ]; [ apply derelict | ]; assumption.
apply rec with (i t3').
destruct rreq as [ rreq ]. apply promote. pose proof (rass rreq) as rass. unfold Ass in rass. destruct (Opt rreq) as [ _ | ]; [ apply derelict | ]; assumption.
revert lreq. apply decidable_ipreprocessingPV'. assumption.
simpl in trec. apply (proof tcon). intro treq. apply trec.
intros t t' trace. apply rec. revert trace. apply trace_comp'. apply recursion with tcon treq. apply assumption.
destruct (Opt treq) as [ preserve | ].
apply preserve. assumption.
apply i_preprocessed.
Qed.
Corollary itrans {t1 t2 t3 : T} : iPreprocessing t1 t2 -> iPreprocessing t2 t3 -> iPreprocessing t1 t3.
intros ed ed' t0 t4 pre d d'. apply @trans with (i t2); try assumption.
apply promote'; try assumption. apply ed; try assumption. apply drefl.
apply ed'; try assumption.
apply i_preprocessed.
apply counit.
Qed.
End Transitivity.
Section Decider.
Theorem decider' (t t' : T) : Preprocessed t -> { Preprocessing t t' } + { Preprocessing t t' -> False }.
apply (fun R rec => i_wf R rec t t'). clear t t'. intros t t' rec pre. destruct (DRule.finite_con t t') as [ lcon finite_req finite ]. assert ({ Preprocessing t t' } + { Forall (fun con : Con t t' => exists req : Req con, Preprocessing (Ass req left) (Ass req right) -> False) lcon }) as inv.
clear finite. induction finite_req as [ | con lcon lreq finite_req ind ]; [ right; apply Forall_nil | ]. destruct ind as [ ind | ind ]; [ left; assumption | ]. destruct lreq as [ lreq finite ]. assert ({ Forall (fun req : Req con => Preprocessing (Ass req left) (Ass req right)) lreq } + { exists req : Req con, Preprocessing (Ass req left) (Ass req right) -> False }) as inv.
clear finite. induction lreq as [ | req lreq rreq ]; [ left; apply Forall_nil | ]. destruct rreq as [ rreq | rreq ]; [ | right; assumption ]. pose proof (rec con req) as rec. destruct rec as [ rec | rec ].
unfold WFI.PRule.Ass. destruct (Opt req) as [ preserve | ].
apply preserve. assumption.
apply i_preprocessed.
left. apply Forall_cons; assumption.
right. apply ex_intro with req. assumption.
destruct inv as [ inv | inv ].
left. apply proof with con. intro req. apply (fun inv => proj1 (Forall_forall _ lreq) inv req) in inv; try assumption. apply finite.
right. apply Forall_cons; assumption.
clear finite_req. destruct inv as [ inv | inv ]; [ left; assumption | ]. right. intro d. assert (Exists (fun con' : Rule.Con t t' => forall req' : Rule.Req con', iPreprocessing (Rule.Ass req' left) (Rule.Ass req' right)) lcon) as fin.
destruct d as [ t t' con ass ]. apply finite with con.
exact iadmitsd.
clear pre. intros t1 t2 t3 t4 d ed d' t0 t5 pre d0 d5. apply ed; try assumption.
revert d0 d. apply dtrans.
revert d' d5. apply dtrans.
intros req t1 t4 pre' d d'. pose proof (ass req) as ass. unfold Ass in ass. destruct (Opt req) as [ preserve | ].
revert d ass d'. apply decidable_trans. assumption.
apply dpromote' in d; try assumption. revert d ass d'. apply decidable_trans. assumption.
clear d finite. induction fin as [ con' lcon d | con' lcon fin ind ].
apply Forall_inv in inv. destruct inv as [ req' nd ]. apply nd. pose proof (d req') as d. apply d.
unfold Ass. destruct (Opt req') as [ preserve | ].
apply preserve. assumption.
apply i_preprocessed.
unfold Ass. destruct (Opt req') as [ _ | ].
apply drefl.
apply counit.
apply drefl.
apply ind. inversion inv. assumption.
Qed.
Corollary decider (t t' : T) : { Preprocessing (i t) t' } + { Preprocessing (i t) t' -> False }.
apply decider'. apply i_preprocessed.
Qed.
End Decider.
End Preprocessing.
This page has been generated by coqdoc