Reductive Subtyping (Decide.v)
For reductive subtyping, the user needs to supply proofs of a few more properties in the module type DecidableRules in order to prove transitivity, decidability and, later (in Convert.v), equivalence to declarative subtyping:- refl: A proof of reflexivity of subtyping, corresponding to the Literal Reflexivity requirement in the paper
- Red: A proof that for all pairs of subtyping rules, where the LHS type of one is equal to the RHS type of the other, there is a way to admit a combined rule. This is corresponds to the Literal Transitivity requirement in the paper
- wf: A well-foundedness proof for the subtyping rules. This corresponds to the Well-Foundedness requirement in the paper
- finite_con: A proof that for every two types, there is a finite number of rules that may apply - this is needed for the proof search algorithm for decidability. This corresponds to the Syntax-Directedness requirement in the paper.
Require Import Common.
Require Import Coq.Lists.List.
Module Type DecidableRules (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule).
Import T.
Import Rule.
Import ORule.
Module Reduction := Reduction T Rule ORule.
Import Reduction.
Module Proof := Reduction.Proof .
Import Proof.
Module ProofPV := Reduction.ProofPV.
Import ProofPV.
Parameter refl : forall t : T, Proof t t.
Parameter Red : forall {t1 t2 t3 : T} (lcon : Con t1 t2) (rcon : Con t2 t3), Reduction lcon rcon.
Parameter 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'.
Parameter finite_con : forall t t' : T, { lcon : list (Con t t')
& Prod (fun con : Con t t' => { lreq : list (Req con) | forall req : Req con, In req lreq }) lcon
& forall R : T -> T -> Prop, Admits R -> (forall {t1 t2 t3 t4 : T}, Proof t1 t2 -> R t2 t3 -> Proof t3 t4 -> R t1 t4) -> forall con : Con t t', (forall req : Req con, R (Ass req left) (Ass req right)) -> Exists (fun con' : Con t t' => forall req' : Req con', R (Ass req' left) (Ass req' right)) lcon }.
End DecidableRules.
Module Decidable (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule).
Import T.
Import Rule.
Import ORule.
Import DRule.
Module Proof := DRule.Proof .
Import Proof.
Module ProofPV := DRule.ProofPV.
Import ProofPV.
Module Reduction := DRule.Reduction.
Import Reduction.
Definition Decidable := Proof.
Definition dproof := proof.
Definition AdmitsD := Admits.
Lemma drefl_R (R : T -> T -> Prop) : AdmitsD R -> forall t : T, R t t.
intros admits t. pose proof (DRule.refl t) as d. revert d. generalize t at 2 4. intros t' d. induction d as [ t t' con _ rec ]. apply (admits _ _ con). assumption.
Qed.
Lemma Red' {t1 t2 t3 : T} (lcon : Con t1 t2) (rcon : Con t2 t3) : ProofPV (Transitivity (Requires lcon) (Requires rcon)) covariant t1 t3.
pose proof (Red lcon rcon) as red. destruct red as [ rreq ev lass e | con ass ].
apply permitV. simpl. apply transr. apply compose with (Ass rreq left).
assumption.
destruct e. rewrite <- ev. apply requires.
apply proofPV with con. assumption.
Qed.
Lemma d_trace_ind (R : T -> T -> Type) : (forall t t' : T, (forall (con : Con t t') (req : Req con) (t t' : T), Trace t t' (Ass req left) (Ass req right) -> R t t') -> R t t') -> forall t t' : T, R t t'.
intros rec t t'. apply rec. apply (fun R rec => wf R rec t t'). clear t t'. intros t t' rec' con req t1 t2 trace. pose proof (rec' con req) as rec'. destruct trace.
apply rec. assumption.
apply rec. intros con' req' t1' t2' trace'. apply rec' with con0 req0. clear rec rec'. revert trace. apply trace_comp. apply recursion with _ req'. assumption.
Qed.
Section Transitivity.
Lemma proofPV_invert_trans (v : Variance) {P P' : Variance -> T -> T -> Prop} : forall {t t' : T}, ProofPV (Transitivity (fun v => P (invert v)) (fun v => P' (invert v))) v t t' -> ProofPV (Transitivity P' P) (invert v) t t'.
apply invertPV'. clear v. intros v t t' trans. destruct trans as [ coma | coma ]; destruct v; destruct coma; simpl in *.
apply transr. apply contrapose with t2; try assumption. apply (@invertPV' covariant) with (fun v => P' (invert v)); try trivial.
apply transr. apply compose with t2; try assumption. apply (@invertPV' contravariant) with (fun v => P' (invert v)); try trivial.
apply transl. apply contrapose with t2; try assumption. apply (@invertPV' covariant) with (fun v => P (invert v)); try trivial.
apply transl. apply compose with t2; try assumption. apply (@invertPV' contravariant) with (fun v => P (invert v)); try trivial.
Qed.
Lemma transPV {P P' : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : ProofPV P covariant t1 t2 -> ProofPV P' covariant t2 t3 -> ProofPV (Transitivity P P') covariant t1 t3.
revert P P' t2. apply (fun R rec => d_trace_ind R rec t1 t3). clear t1 t3. intros t1 t3 rec P P' t2 p p'. remember covariant as v in p'. induction p' as [ v t2 t3 p' | v t2 t3 rcon rass rrec ]; subst.
apply permitV. apply transr. apply compose with t2; assumption.
assert (forall v t t', Requires rcon v t t' -> ProofPV P' v t t') as rass'.
intros v t t' rreq. destruct rreq as [ rreq ]. apply rass.
remember covariant as v in p. destruct p as [ v t1 t2 p | v t1 t2 lcon lass ]; subst.
apply permitV. apply transl. apply compose with t2; try assumption. apply (proofPV _ rcon). assumption.
assert (forall v t t', Requires lcon v t t' -> ProofPV P v t t') as lass'.
intros v t t' lreq. destruct lreq as [ lreq ]. apply lass.
pose proof (Red lcon rcon) as red. destruct red as [ rreq ev lreq e | con ass ].
pose proof (rrec rreq) as rrec. rewrite ev in rrec. rewrite multiply_covariant in rrec. rewrite <- e. apply rrec.
rewrite e. assumption.
revert lreq. apply bindV. assumption.
reflexivity.
apply (proofPV _ con). intro req. pose proof (ass req) as ass. pose proof (rec _ req) as rec. revert rec. simpl. induction ass as [ v t1' t3' trans | v t1' t3' con' ass' rec' ]; intro rec; simpl in *.
destruct trans as [ coma | coma]; destruct v; simpl in coma.
destruct coma as [ t2' lreq rreq ]. remember covariant as v. destruct lreq as [ lreq ]. apply rec with (Ass lreq right).
apply assumption.
apply lass.
revert rreq. apply bindV. assumption.
destruct coma as [ t2' rreq lreq ]. apply (proofPV_invert_trans covariant). remember contravariant as v in lreq. destruct lreq as [ lreq ]. apply rec with (Ass lreq left).
apply assumption.
apply (invertPV contravariant). revert rreq. apply bindV. assumption.
apply (invertPV contravariant). rewrite <- Heqv. apply lass.
destruct coma as [ t2' lreq rreq ]. remember covariant as v. destruct rreq as [ rreq ]. apply rec with (Ass rreq left).
apply assumption.
revert lreq. apply bindV. assumption.
apply rass.
destruct coma as [ t2' rreq lreq ]. apply (proofPV_invert_trans covariant). remember contravariant as v in rreq. destruct rreq as [ rreq ]. apply rec with (Ass rreq right).
apply assumption.
apply (invertPV contravariant). rewrite <- Heqv. apply rass.
apply (invertPV contravariant). revert lreq. apply bindV. assumption.
apply (proofPV _ con'). intro req'. apply rec'. intros t1'' t2'' trace. apply rec. apply recursion with _ req'. assumption.
Qed.
Lemma transPV' {P P' Pt : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity P P' v t t' -> Pt v t t') -> ProofPV P covariant t1 t2 -> ProofPV P' covariant t2 t3 -> ProofPV Pt covariant t1 t3.
intros trans p p'. apply @monoV with (Transitivity P P'); try assumption. revert p p'. apply transPV.
Qed.
Lemma trans_bindV {P P' Pt : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity P P' v t t' -> ProofPV Pt v t t') -> ProofPV P covariant t1 t2 -> ProofPV P' covariant t2 t3 -> ProofPV Pt covariant t1 t3.
intros trans p p'. apply bindV with (Transitivity P P'); try assumption. revert p p'. apply transPV.
Qed.
Lemma trans_contra {P P' : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : ProofPV P contravariant t1 t2 -> ProofPV P' contravariant t2 t3 -> ProofPV (Transitivity P' P) contravariant t1 t3.
intros p p'. apply (proofPV_invert_trans covariant). apply invertPV in p. apply invertPV in p'. revert p p'. apply transPV.
Qed.
Lemma trans_contra' {P P' Pt : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity P' P v t t' -> Pt v t t') -> ProofPV P contravariant t1 t2 -> ProofPV P' contravariant t2 t3 -> ProofPV Pt contravariant t1 t3.
intros trans p p'. apply @monoV with (Transitivity P' P); try assumption. apply (proofPV_invert_trans covariant). apply invertPV in p. apply invertPV in p'. revert p p'. apply transPV.
Qed.
Lemma trans_bind_contra {P P' Pt : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity P' P v t t' -> ProofPV Pt v t t') -> ProofPV P contravariant t1 t2 -> ProofPV P' contravariant t2 t3 -> ProofPV Pt contravariant t1 t3.
intros trans p p'. apply bindV with (Transitivity P' P); try assumption. revert p p'. apply trans_contra.
Qed.
Lemma trans_bind {P P' Pt : T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity (fun v => P) (fun v => P') v t t' -> ProofP Pt t t') -> ProofP P t1 t2 -> ProofP P' t2 t3 -> ProofP Pt t1 t3.
intros trans p p'. apply (proofP_proofPV covariant) in p. apply (proofP_proofPV covariant) in p'. apply (@proofPV_proofP covariant). revert p p'. apply trans_bindV. clear t1 t2 t3. intros v t1 t3 t. apply proofP_proofPV. apply trans with v. assumption.
Qed.
Lemma trans {t1 t2 t3 : T} : Proof t1 t2 -> Proof t2 t3 -> Proof t1 t3.
intros p p'. apply (proof_proofPV covariant) in p. apply (proof_proofPV covariant) in p'. apply (@proofPV_proof covariant). revert p p'. apply transPV'. clear t1 t2 t3. intros v t t' trans. destruct trans as [ coma | coma ]; destruct v; destruct coma as [ t2 p p' ]; (destruct p; fail || destruct p'; fail).
Qed.
End Transitivity.
Require Import Coq.Lists.List.
Module Type DecidableRules (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule).
Import T.
Import Rule.
Import ORule.
Module Reduction := Reduction T Rule ORule.
Import Reduction.
Module Proof := Reduction.Proof .
Import Proof.
Module ProofPV := Reduction.ProofPV.
Import ProofPV.
Parameter refl : forall t : T, Proof t t.
Parameter Red : forall {t1 t2 t3 : T} (lcon : Con t1 t2) (rcon : Con t2 t3), Reduction lcon rcon.
Parameter 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'.
Parameter finite_con : forall t t' : T, { lcon : list (Con t t')
& Prod (fun con : Con t t' => { lreq : list (Req con) | forall req : Req con, In req lreq }) lcon
& forall R : T -> T -> Prop, Admits R -> (forall {t1 t2 t3 t4 : T}, Proof t1 t2 -> R t2 t3 -> Proof t3 t4 -> R t1 t4) -> forall con : Con t t', (forall req : Req con, R (Ass req left) (Ass req right)) -> Exists (fun con' : Con t t' => forall req' : Req con', R (Ass req' left) (Ass req' right)) lcon }.
End DecidableRules.
Module Decidable (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule).
Import T.
Import Rule.
Import ORule.
Import DRule.
Module Proof := DRule.Proof .
Import Proof.
Module ProofPV := DRule.ProofPV.
Import ProofPV.
Module Reduction := DRule.Reduction.
Import Reduction.
Definition Decidable := Proof.
Definition dproof := proof.
Definition AdmitsD := Admits.
Lemma drefl_R (R : T -> T -> Prop) : AdmitsD R -> forall t : T, R t t.
intros admits t. pose proof (DRule.refl t) as d. revert d. generalize t at 2 4. intros t' d. induction d as [ t t' con _ rec ]. apply (admits _ _ con). assumption.
Qed.
Lemma Red' {t1 t2 t3 : T} (lcon : Con t1 t2) (rcon : Con t2 t3) : ProofPV (Transitivity (Requires lcon) (Requires rcon)) covariant t1 t3.
pose proof (Red lcon rcon) as red. destruct red as [ rreq ev lass e | con ass ].
apply permitV. simpl. apply transr. apply compose with (Ass rreq left).
assumption.
destruct e. rewrite <- ev. apply requires.
apply proofPV with con. assumption.
Qed.
Lemma d_trace_ind (R : T -> T -> Type) : (forall t t' : T, (forall (con : Con t t') (req : Req con) (t t' : T), Trace t t' (Ass req left) (Ass req right) -> R t t') -> R t t') -> forall t t' : T, R t t'.
intros rec t t'. apply rec. apply (fun R rec => wf R rec t t'). clear t t'. intros t t' rec' con req t1 t2 trace. pose proof (rec' con req) as rec'. destruct trace.
apply rec. assumption.
apply rec. intros con' req' t1' t2' trace'. apply rec' with con0 req0. clear rec rec'. revert trace. apply trace_comp. apply recursion with _ req'. assumption.
Qed.
Section Transitivity.
Lemma proofPV_invert_trans (v : Variance) {P P' : Variance -> T -> T -> Prop} : forall {t t' : T}, ProofPV (Transitivity (fun v => P (invert v)) (fun v => P' (invert v))) v t t' -> ProofPV (Transitivity P' P) (invert v) t t'.
apply invertPV'. clear v. intros v t t' trans. destruct trans as [ coma | coma ]; destruct v; destruct coma; simpl in *.
apply transr. apply contrapose with t2; try assumption. apply (@invertPV' covariant) with (fun v => P' (invert v)); try trivial.
apply transr. apply compose with t2; try assumption. apply (@invertPV' contravariant) with (fun v => P' (invert v)); try trivial.
apply transl. apply contrapose with t2; try assumption. apply (@invertPV' covariant) with (fun v => P (invert v)); try trivial.
apply transl. apply compose with t2; try assumption. apply (@invertPV' contravariant) with (fun v => P (invert v)); try trivial.
Qed.
Lemma transPV {P P' : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : ProofPV P covariant t1 t2 -> ProofPV P' covariant t2 t3 -> ProofPV (Transitivity P P') covariant t1 t3.
revert P P' t2. apply (fun R rec => d_trace_ind R rec t1 t3). clear t1 t3. intros t1 t3 rec P P' t2 p p'. remember covariant as v in p'. induction p' as [ v t2 t3 p' | v t2 t3 rcon rass rrec ]; subst.
apply permitV. apply transr. apply compose with t2; assumption.
assert (forall v t t', Requires rcon v t t' -> ProofPV P' v t t') as rass'.
intros v t t' rreq. destruct rreq as [ rreq ]. apply rass.
remember covariant as v in p. destruct p as [ v t1 t2 p | v t1 t2 lcon lass ]; subst.
apply permitV. apply transl. apply compose with t2; try assumption. apply (proofPV _ rcon). assumption.
assert (forall v t t', Requires lcon v t t' -> ProofPV P v t t') as lass'.
intros v t t' lreq. destruct lreq as [ lreq ]. apply lass.
pose proof (Red lcon rcon) as red. destruct red as [ rreq ev lreq e | con ass ].
pose proof (rrec rreq) as rrec. rewrite ev in rrec. rewrite multiply_covariant in rrec. rewrite <- e. apply rrec.
rewrite e. assumption.
revert lreq. apply bindV. assumption.
reflexivity.
apply (proofPV _ con). intro req. pose proof (ass req) as ass. pose proof (rec _ req) as rec. revert rec. simpl. induction ass as [ v t1' t3' trans | v t1' t3' con' ass' rec' ]; intro rec; simpl in *.
destruct trans as [ coma | coma]; destruct v; simpl in coma.
destruct coma as [ t2' lreq rreq ]. remember covariant as v. destruct lreq as [ lreq ]. apply rec with (Ass lreq right).
apply assumption.
apply lass.
revert rreq. apply bindV. assumption.
destruct coma as [ t2' rreq lreq ]. apply (proofPV_invert_trans covariant). remember contravariant as v in lreq. destruct lreq as [ lreq ]. apply rec with (Ass lreq left).
apply assumption.
apply (invertPV contravariant). revert rreq. apply bindV. assumption.
apply (invertPV contravariant). rewrite <- Heqv. apply lass.
destruct coma as [ t2' lreq rreq ]. remember covariant as v. destruct rreq as [ rreq ]. apply rec with (Ass rreq left).
apply assumption.
revert lreq. apply bindV. assumption.
apply rass.
destruct coma as [ t2' rreq lreq ]. apply (proofPV_invert_trans covariant). remember contravariant as v in rreq. destruct rreq as [ rreq ]. apply rec with (Ass rreq right).
apply assumption.
apply (invertPV contravariant). rewrite <- Heqv. apply rass.
apply (invertPV contravariant). revert lreq. apply bindV. assumption.
apply (proofPV _ con'). intro req'. apply rec'. intros t1'' t2'' trace. apply rec. apply recursion with _ req'. assumption.
Qed.
Lemma transPV' {P P' Pt : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity P P' v t t' -> Pt v t t') -> ProofPV P covariant t1 t2 -> ProofPV P' covariant t2 t3 -> ProofPV Pt covariant t1 t3.
intros trans p p'. apply @monoV with (Transitivity P P'); try assumption. revert p p'. apply transPV.
Qed.
Lemma trans_bindV {P P' Pt : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity P P' v t t' -> ProofPV Pt v t t') -> ProofPV P covariant t1 t2 -> ProofPV P' covariant t2 t3 -> ProofPV Pt covariant t1 t3.
intros trans p p'. apply bindV with (Transitivity P P'); try assumption. revert p p'. apply transPV.
Qed.
Lemma trans_contra {P P' : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : ProofPV P contravariant t1 t2 -> ProofPV P' contravariant t2 t3 -> ProofPV (Transitivity P' P) contravariant t1 t3.
intros p p'. apply (proofPV_invert_trans covariant). apply invertPV in p. apply invertPV in p'. revert p p'. apply transPV.
Qed.
Lemma trans_contra' {P P' Pt : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity P' P v t t' -> Pt v t t') -> ProofPV P contravariant t1 t2 -> ProofPV P' contravariant t2 t3 -> ProofPV Pt contravariant t1 t3.
intros trans p p'. apply @monoV with (Transitivity P' P); try assumption. apply (proofPV_invert_trans covariant). apply invertPV in p. apply invertPV in p'. revert p p'. apply transPV.
Qed.
Lemma trans_bind_contra {P P' Pt : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity P' P v t t' -> ProofPV Pt v t t') -> ProofPV P contravariant t1 t2 -> ProofPV P' contravariant t2 t3 -> ProofPV Pt contravariant t1 t3.
intros trans p p'. apply bindV with (Transitivity P' P); try assumption. revert p p'. apply trans_contra.
Qed.
Lemma trans_bind {P P' Pt : T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity (fun v => P) (fun v => P') v t t' -> ProofP Pt t t') -> ProofP P t1 t2 -> ProofP P' t2 t3 -> ProofP Pt t1 t3.
intros trans p p'. apply (proofP_proofPV covariant) in p. apply (proofP_proofPV covariant) in p'. apply (@proofPV_proofP covariant). revert p p'. apply trans_bindV. clear t1 t2 t3. intros v t1 t3 t. apply proofP_proofPV. apply trans with v. assumption.
Qed.
Lemma trans {t1 t2 t3 : T} : Proof t1 t2 -> Proof t2 t3 -> Proof t1 t3.
intros p p'. apply (proof_proofPV covariant) in p. apply (proof_proofPV covariant) in p'. apply (@proofPV_proof covariant). revert p p'. apply transPV'. clear t1 t2 t3. intros v t t' trans. destruct trans as [ coma | coma ]; destruct v; destruct coma as [ t2 p p' ]; (destruct p; fail || destruct p'; fail).
Qed.
End Transitivity.
Section Decider.
Lemma decider (t t' : T) : { Decidable t t' } + { Decidable t t' -> False }.
apply (fun R rec => wf R rec t t'). clear t t'. intros t t' rec. destruct (finite_con t t') as [ lcon finite_req finite ]. assert ({ Decidable t t' } + { Forall (fun con : Con t t' => exists req : Req con, Decidable (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 inl ]. assert ({ Forall (fun req : Req con => Decidable (Ass req left) (Ass req right)) lreq } + { exists req : Req con, Decidable (Ass req left) (Ass req right) -> False }) as inv.
clear inl. induction lreq as [ | req lreq ]; [ left; apply Forall_nil | ]. destruct IHlreq as [ IHlreq | IHlreq ]; [ | right; assumption ]. destruct (rec con req) as [ d | nd ].
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 inl.
right. apply Forall_cons; assumption.
clear finite_req. destruct inv as [ inv | inv ].
left. assumption.
right. intro d. pose proof (finite Decidable proof_admits (fun t1 t2 t3 t4 d1 d2 d3 => trans d1 (trans d2 d3))) as finite. destruct d as [ t t' con ass ]. pose proof (finite con ass) as finite. induction finite as [ con' lcon d | con' lcon finite ind ] .
apply Forall_inv in inv. destruct inv as [ req' nd ]. apply nd. apply d.
apply ind. inversion inv. assumption.
Qed.
End Decider.
End Decidable.
Lemma decider (t t' : T) : { Decidable t t' } + { Decidable t t' -> False }.
apply (fun R rec => wf R rec t t'). clear t t'. intros t t' rec. destruct (finite_con t t') as [ lcon finite_req finite ]. assert ({ Decidable t t' } + { Forall (fun con : Con t t' => exists req : Req con, Decidable (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 inl ]. assert ({ Forall (fun req : Req con => Decidable (Ass req left) (Ass req right)) lreq } + { exists req : Req con, Decidable (Ass req left) (Ass req right) -> False }) as inv.
clear inl. induction lreq as [ | req lreq ]; [ left; apply Forall_nil | ]. destruct IHlreq as [ IHlreq | IHlreq ]; [ | right; assumption ]. destruct (rec con req) as [ d | nd ].
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 inl.
right. apply Forall_cons; assumption.
clear finite_req. destruct inv as [ inv | inv ].
left. assumption.
right. intro d. pose proof (finite Decidable proof_admits (fun t1 t2 t3 t4 d1 d2 d3 => trans d1 (trans d2 d3))) as finite. destruct d as [ t t' con ass ]. pose proof (finite con ass) as finite. induction finite as [ con' lcon d | con' lcon finite ind ] .
apply Forall_inv in inv. destruct inv as [ req' nd ]. apply nd. apply d.
apply ind. inversion inv. assumption.
Qed.
End Decider.
End Decidable.
This page has been generated by coqdoc