From 061af1379740c1118e42ae7c37ea294b4c2174f3 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 7 Mar 2011 05:41:33 -0800 Subject: [PATCH] add proper proofs of the fact that every rule has exactly one conclusion --- src/HaskProof.v | 81 ++++++++++++++++++++++++++++++++++++++++++++++++ src/HaskProofToLatex.v | 2 -- 2 files changed, 81 insertions(+), 2 deletions(-) diff --git a/src/HaskProof.v b/src/HaskProof.v index 87dfe2e..606b667 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -135,4 +135,85 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c) := @nd_map' _ (@URule Γ Δ ) _ Rule (@UJudg2judg Γ Δ ) (fun h c r => nd_rule (RURule _ _ h c r)) h c. +Lemma no_urules_with_empty_conclusion : forall Γ Δ c h, @URule Γ Δ c h -> h=[] -> False. + intro. + intro. + induction 1; intros; inversion H. + simpl in *; destruct c; try destruct o; simpl in *; try destruct u; inversion H; simpl in *; apply IHX; auto; inversion H1. + simpl in *; destruct c; try destruct o; simpl in *; try destruct u; inversion H; simpl in *; apply IHX; auto; inversion H1. + Qed. + +Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False. + intros. + destruct X; try destruct c; try destruct o; simpl in *; try inversion H. + apply no_urules_with_empty_conclusion in u. + apply u. + auto. + Qed. + +Lemma no_urules_with_multiple_conclusions : forall Γ Δ c h, + @URule Γ Δ c h -> { h1:Tree ??(UJudg Γ Δ) & { h2:Tree ??(UJudg Γ Δ) & h=(h1,,h2) }} -> False. + intro. + intro. + induction 1; intros. + inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + + apply IHX. + destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *. + inversion e. + inversion e. + exists c1. exists c2. auto. + + apply IHX. + destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *. + inversion e. + inversion e. + exists c1. exists c2. auto. + + inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + Qed. + +Lemma no_rules_with_multiple_conclusions : forall c h, + Rule c h -> { h1:Tree ??Judg & { h2:Tree ??Judg & h=(h1,,h2) }} -> False. + intros. + destruct X; try destruct c; try destruct o; simpl in *; try inversion H; + try apply no_urules_with_empty_conclusion in u; try apply u. + destruct X0; destruct s; inversion e. + auto. + apply (no_urules_with_multiple_conclusions _ _ h (c1,,c2)) in u. inversion u. exists c1. exists c2. auto. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + Qed. + +Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False. + intros. + eapply no_rules_with_multiple_conclusions. + apply r. + exists c1. + exists c2. + auto. + Qed. + diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index 55496dc..e239205 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -206,8 +206,6 @@ Section ToLatex. end. End ToLatex. -Axiom systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False. - Definition nd_ml_toLatex {c}(pf:@ND _ Rule [] c) := @SCND_toLatex _ _ judgment2latex -- 1.7.10.4