From 5c0ced5c13852bcc93761859285efe4c5f0d2513 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 22 Sep 2008 12:19:29 +0000 Subject: [PATCH] new small devel --- .../matita/contribs/character/Makefile | 16 +++ .../matita/contribs/character/classes/defs.ma | 23 ++++ .../contribs/character/classes/props_pt.ma | 108 ++++++++++++++++++ .../matita/contribs/character/depends | 5 + .../matita/contribs/character/preamble.ma | 82 +++++++++++++ helm/software/matita/contribs/character/root | 1 + 6 files changed, 235 insertions(+) create mode 100644 helm/software/matita/contribs/character/Makefile create mode 100644 helm/software/matita/contribs/character/classes/defs.ma create mode 100644 helm/software/matita/contribs/character/classes/props_pt.ma create mode 100644 helm/software/matita/contribs/character/depends create mode 100644 helm/software/matita/contribs/character/preamble.ma create mode 100644 helm/software/matita/contribs/character/root diff --git a/helm/software/matita/contribs/character/Makefile b/helm/software/matita/contribs/character/Makefile new file mode 100644 index 000000000..a3e891435 --- /dev/null +++ b/helm/software/matita/contribs/character/Makefile @@ -0,0 +1,16 @@ +include ../Makefile.defs + +DIR=$(shell basename $$PWD) + +$(DIR) all: + $(BIN)matitac +$(DIR).opt opt all.opt: + $(BIN)matitac.opt +clean: + $(BIN)matitaclean +clean.opt: + $(BIN)matitaclean.opt +depend: + $(BIN)matitadep +depend.opt: + $(BIN)matitadep.opt diff --git a/helm/software/matita/contribs/character/classes/defs.ma b/helm/software/matita/contribs/character/classes/defs.ma new file mode 100644 index 000000000..e31c9a93c --- /dev/null +++ b/helm/software/matita/contribs/character/classes/defs.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "preamble.ma". + +inductive P: nat \to Prop \def + | p1: P 1 + | p2: \forall i,j. T i \to P j \to P (i + j) +with T: nat \to Prop \def + | t1: \forall i. P i \to T (i * 3) + | t2: \forall i. T i \to T (i * 3) +. diff --git a/helm/software/matita/contribs/character/classes/props_pt.ma b/helm/software/matita/contribs/character/classes/props_pt.ma new file mode 100644 index 000000000..cc1c449a3 --- /dev/null +++ b/helm/software/matita/contribs/character/classes/props_pt.ma @@ -0,0 +1,108 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "classes/defs.ma". + +theorem p_inv_O: P 0 \to False. + intros; inversion H; clear H; intros; + [ destruct + | lapply linear plus_inv_O3 to H3; decompose; destruct; + autobatch depth = 2 + ]. +qed. + +theorem t_inv_O: T 0 \to False. + intros; inversion H; clear H; intros; + [ lapply linear times_inv_O3_S to H1; destruct; autobatch depth = 2 + | lapply linear times_inv_O3_S to H2; destruct; autobatch depth = 2 + ]. +qed. + +theorem p_pos: \forall i. P i \to \exists k. i = S k. + intros 1; elim i names 0; clear i; intros; + [ lapply linear p_inv_O to H; decompose + | autobatch depth = 2 + ]. +qed. + +theorem t_pos: \forall i. T i \to \exists k. i = S k. + intros 1; elim i names 0; clear i; intros; + [ lapply linear t_inv_O to H; decompose + | autobatch depth = 2 + ]. +qed. + +theorem t_1: T 1 \to False. + intros; inversion H; clear H; intros; + [ lapply not_3_divides_1 to H1; decompose + | lapply not_3_divides_1 to H2; decompose + ]. +qed. + +theorem t_3: T 3. + change in \vdash (? %) with (1 * 3); + autobatch depth = 2. +qed. + +theorem pt_inv_gen: \forall i. + (P i \to \exists h. i = S (h * 3)) \land + (T i \to \exists h,k. i = S (h * 3) * 3 \sup (S k)). + intros 1; elim i using wf_nat_ind names 0; clear i; intros; split; intros; + [ lapply linear p_inv_O to H; decompose + | lapply linear t_inv_O to H; decompose + | inversion H1; clear H1; intros; + [ destruct; autobatch depth = 3 + | clear H3; lapply t_pos to H1; lapply p_pos to H2; decompose; destruct; + lapply linear plus_inv_S_S_S to H4; decompose; + lapply H to H4; lapply H to H3; clear H H4 H3; decompose; clear H3 H4; + lapply linear H to H2; lapply linear H5 to H1; decompose; + rewrite > H; rewrite > H2; clear H H2; + rewrite < plus_n_Sm; rewrite > times_exp_x_y_Sz; autobatch depth = 2 + ] + | inversion H1; clear H1; intros; + [ lapply linear times_inv_S_m_SS to H2 as H0; + lapply linear H to H0; decompose; clear H2; + lapply linear H to H1; decompose; destruct; + autobatch depth = 4 + | clear H2; lapply linear times_inv_S_m_SS to H3 as H0; + lapply linear H to H0; decompose; clear H; + lapply linear H2 to H1; decompose; destruct; + autobatch depth = 3 + ] + ]. +qed. + +theorem p_inv_gen: \forall i. P i \to \exists h. i = S (h * 3). + intros; lapply depth = 1 pt_inv_gen; decompose; + lapply linear H1 to H as H0; autobatch depth = 1. +qed. + +theorem t_inv_gen: \forall i. T i \to \exists h,k. i = (S (h * 3)) * 3 \sup (S k). + intros; lapply depth = 1 pt_inv_gen; decompose; + lapply linear H2 to H as H0; autobatch depth = 2. +qed. + +theorem p_gen: \forall i. P (S (i * 3)). + intros; elim i names 0; clear i; intros; + [ simplify; autobatch depth = 2 + | rewrite > plus_3_S3n ; autobatch depth = 2 + ]. +qed. + +theorem t_gen: \forall i,j. T (S (i * 3) * 3 \sup (S j)). + intros; elim j names 0; clear j; intros; + [ simplify in \vdash (? (? ? %)); autobatch depth = 2 + | rewrite > times_exp_x_y_Sz; autobatch depth = 2 + ]. +qed. diff --git a/helm/software/matita/contribs/character/depends b/helm/software/matita/contribs/character/depends new file mode 100644 index 000000000..7079205b1 --- /dev/null +++ b/helm/software/matita/contribs/character/depends @@ -0,0 +1,5 @@ +preamble.ma nat/exp.ma nat/relevant_equations.ma +classes/defs.ma preamble.ma +classes/props_pt.ma classes/defs.ma +nat/exp.ma +nat/relevant_equations.ma diff --git a/helm/software/matita/contribs/character/preamble.ma b/helm/software/matita/contribs/character/preamble.ma new file mode 100644 index 000000000..ac3f19c6e --- /dev/null +++ b/helm/software/matita/contribs/character/preamble.ma @@ -0,0 +1,82 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "nat/exp.ma". +include "nat/relevant_equations.ma". + +alias num (instance 0) = "natural number". + +theorem plus_inv_O3: \forall m,n. 0 = n + m \to 0 = n \land 0 = m. + intros 2; elim n names 0; clear n; simplify; intros; + [ autobatch | destruct ]. +qed. + +theorem times_inv_O3_S: \forall x,y. 0 = x * (S y) -> x = 0. + intros; rewrite < times_n_Sm in H; + lapply linear plus_inv_O3 to H; decompose; destruct; autobatch. +qed. + +theorem not_3_divides_1: \forall n. 1 = n * 3 \to False. + intros 1; rewrite > sym_times; simplify; + elim n names 0; simplify; intros; destruct; + rewrite > sym_plus in Hcut; simplify in Hcut; destruct Hcut. +qed. + +theorem le_inv_S_S: \forall m,n. S m <= S n \to m <= n. + intros; inversion H; clear H; intros; destruct; autobatch. +qed. + +theorem plus_inv_S_S_S: \forall x,y,z. S x = S y + S z \to S y <= x \land S z <= x. + simplify; intros; destruct; + rewrite < plus_n_Sm in \vdash (? (? ? %) ?); autobatch depth = 3. +qed. + +theorem times_inv_S_m_SS: \forall k,n,m. S n = m * (S (S k)) \to m \le n. + intros 3; elim m names 0; clear m; simplify; intros; destruct; + clear H; apply le_S_S; rewrite < sym_times; simplify; + autobatch depth = 2. +qed. + +theorem plus_3_S3n: \forall n. S (S n * 3) = 3 + S (n * 3). + intros; simplify; autobatch. +qed. + +theorem times_exp_x_y_Sz: \forall x,y,z. x * y \sup (S z) = (x * y \sup z) * y. + intros; simplify; autobatch depth = 1. +qed. + +definition acc_nat \def \lambda P:nat \to Prop. \lambda n. + \forall m. m <= n \to P m. + +theorem wf_le: \forall P. + P 0 \to (\forall n. acc_nat P n \to P (S n)) \to + \forall n. acc_nat P n. + unfold acc_nat; intros 4; elim n names 0; clear n; + [ intros; lapply linear le_n_O_to_eq to H2; destruct; autobatch + | intros 3; elim m; clear m; intros; clear H3; + [ clear H H1; autobatch + | clear H; lapply linear le_inv_S_S to H4; + apply H1; clear H1; intros; + apply H2; clear H2; autobatch depth = 2 + ] + ]. +qed. + +theorem wf_nat_ind: \forall P:nat \to Prop. + P O \to + (\forall n. (\forall m. m <= n \to P m) \to P (S n)) \to + \forall n. P n. + intros; lapply linear depth=2 wf_le to H, H1 as H0; + unfold acc_nat in H0; apply (H0 n n); autobatch. +qed. diff --git a/helm/software/matita/contribs/character/root b/helm/software/matita/contribs/character/root new file mode 100644 index 000000000..059686b38 --- /dev/null +++ b/helm/software/matita/contribs/character/root @@ -0,0 +1 @@ +baseuri=cic:/matita/character -- 2.39.2