--- /dev/null
+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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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)
+.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+baseuri=cic:/matita/character
projects / helm.git / commitdiff