proposition: Lemma hilbert_soundness A : gen A -> prv ([af A.1] ---> interp_a A.2 ---> Bot).
proof: Proof. elim => {A} /=. - move => C E. rewrite -> andU, afp1. rule axAcase. exact: axBE. - move => p C E. rewrite -> andU,andU,afp1,afn1. rule axAcase. Intro. ApplyH axAcase; do 3 Intro. Apply* 2. - move => s t C E _ IHs _ IHt. rewrite -> andU, afp1. rule axAcase. Intro. Have (~~: s :\/: t). ApplyH axIO. drop. rule axOE. + rewrite <- IHs. rewrite -> andU,af1n. exact: axAI. + rewrite <- IHt. rewrite -> andU. rewrite -> (af1p t) at 1. exact: axAI. - move => s t C R _ IH. rewrite <- IH. do ! rewrite -> andU. rewrite -> afn1, <- af1p, <- af1n. rewrite -> dmI, axAA. exact: axI. - move => s C E _ IH. rewrite -> andU,afn1. rewrite -> box_request, annot_request. rewrite <- (axDN s); rewrite -/(EX (~~: s)). rule axAcase. do 3 Intro. Have (EX ( ~~: s :/\: (interp_a (aR E) :/\: [af R C]))). ApplyH axDBD. rewrite <- axABBA. by ApplyH axAI. drop. rewrite <- axDF. apply: rEXn. rule axAcase. Intro. ApplyH axAcase; do 2 Intro. ApplyH IH. rewrite -> andU, <- af1n. ApplyH axAI. - move => s t C E _ IH1 _ IH2. rewrite -> andU, afp1, axAUeq. rewrite -> axADr. rule axOE. + by rewrite -> (af1p t), <- andU. + rewrite -> (af1p s) at 1. rewrite -> (af1p (AX (AU s t))). do 2 rewrite <- andU. by rewrite -fsetUA. - move => s t C R _ IH1 _ IH2. rewrite -> andU,afn1. rewrite -> axAC. rule axAcase. Intro. rewrite -> (dmAU s t), axERu. ApplyH axAcase; Intro. ApplyH axOE; Intro. - ApplyH IH1. do ! rewrite -> andU. do ! rewrite <- af1n. do ! ApplyH axAI. - ApplyH IH2. do ! rewrite -> andU. do ! rewrite <- af1n. ApplyH axAI. ApplyH axAI. Rev. drop. do 2 Intro. Have (EX (ER (~~: s) (~~: t) :/\: fAU s t)). by ApplyH axDBD. drop. rewrite -> axAC, axAUERF. exact: axDF. - move => s t C _ IH. rewrite -> andU, afp1. do ! rewrite <- hist0 in IH. rule axAcase. do 3 Intro. by ApplyH IH. - move => s t H C _ IH1 _ IH2. apply: AUH_hil. + rule axAcase. do 2 Intro. ApplyH IH1. rewrite -> andU, <- af1p. ApplyH axAI. exact: axsT. + rewrite /AU_. rewrite <- histU. do 3 Intro. ApplyH IH2. rewrite -> andU, <- af1p. by ApplyH axAI. - move => s t H C. rewrite -> axAUAEr, histU. rewrite -> axAEl. do 2 Intro. Apply. - move => s t C E _ IH1 _ IH2. rewrite -> andU,afp1. rewrite -> axAReq. do 2 rule axAcase. rule axC. rule axOE. + do 3 Intro. ApplyH IH1. do 2 rewrite -> andU. do 2 rewrite <- af1p. by do 2 ApplyH axAI. + do 3 Intro. ApplyH IH2. do 2 rewrite -> andU. do 2 rewrite <- af1p. by do 2 ApplyH axAI. - move => s t C E _ IH1 _ IH2. rewrite -> andU,afn1. rewrite -> (dmAR s t). rewrite -> axEUeq. rule axAcase. rule axOE. + do 3 Intro. ApplyH IH1. rewrite -> andU. rewrite <- af1n. by ApplyH axAI. + rule axAcase. do 3 Intro. ApplyH IH2. do 2 rewrite -> andU. do 2 rewrite <- af1n. rewrite /=. rewrite -> dmAX. rewrite -> dmAR. by do 2 ApplyH axAI. - move => s t C _ IH. rewrite -> andU,afn1 => /=. rewrite -> dmAR. rule axAcase. do 3 Intro. do 2 rewrite <- hist0 in IH. by ApplyH IH. - move => s t H C _ IH1 _ IH2. apply: ARH_hil. - rewrite -> andU in IH1. do 2 Intro. ApplyH IH1; last by drop; exact: axI. rewrite <- af1n. by ApplyH axAI. - rewrite /EU_. rewrite <- histU. do 3 Intro. ApplyH IH2. rewrite -> andU. rewrite <- af1n. by ApplyH axAI. - move => s t H C. rewrite -> axEUEr. rewrite -> histU,axAEl. exact: axContra. - move => s t H C _ IH. rewrite -> box_request. do 2 Intro. Suff (EX fF). drop. Intro. Apply. drop. exact: axBT. Suff (EX ([af R C] :/\: EU (~~: s :/\: hist H) (~~: t :/\: hist H))). drop. apply: rEXn. by rule axAcase. rewrite <- (axAC _ [af R C]). ApplyH axDBD. - move => C E _ IH. rewrite -> box_request, annot_request. do 2 Intro. Have (~~: fAX fF). ApplyH ax_serial. rewrite <- (axDN fF) at 1; rewrite -/(EX Top). Intro. Have (EX ( Top :/\: (interp_a (aR E) :/\: [af R C]))). ApplyH axDBD. rewrite <- axABBA. by ApplyH axAI. drop. rewrite <- axDF. apply: rEXn. rule axAcase. drop. rule axAcase; do 2 Intro. Rev* 1. Rev. done. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.CTL(CTL_def gen_def hilbert hilbert_hist)