(**************************************************************************)
(* ___ *)
(* ||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 *)
(* *)
(**************************************************************************)
(* This file was automatically generated: do not edit *********************)
include "CoRN.ma".
(* $Id: Basics.v,v 1.7 2004/04/09 15:58:31 lcf Exp $ *)
(*#* printing alpha %\ensuremath{\alpha}% #α# *)
(*#* printing beta %\ensuremath{\beta}% #β# *)
(*#* printing delta %\ensuremath{\delta}% #δ# *)
(*#* printing eps %\ensuremath{\varepsilon}% #ε# *)
(*#* printing phi %\ensuremath{\phi}% #φ# *)
(*#* printing eta %\ensuremath{\eta}% #η# *)
(*#* printing omega %\ensuremath{\omega}% #ω# *)
(*#* printing nat %\ensuremath{\mathbb N}% #N# *)
(*#* printing Z %\ensuremath{\mathbb Z}% #Z# *)
include "algebra/ListType.ma".
(*#* *Basics
This is random stuff that should be in the Coq basic library.
*)
inline procedural "cic:/CoRN/algebra/Basics/lt_le_dec.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/lt_z_two.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/le_pred.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/lt_mult_right.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/le_mult_right.con" as lemma.
(*#* The power function does not exist in the standard library *)
inline procedural "cic:/CoRN/algebra/Basics/power.con" as definition.
(*#* Factorial function. Does not exist in Arith.
Needed for special operations on polynomials. *)
inline procedural "cic:/CoRN/algebra/Basics/fac.con" as definition.
inline procedural "cic:/CoRN/algebra/Basics/nat_fac_gtzero.con" as lemma.
(* needed for computational behavior of "Inversion" tactic *)
(* UNEXPORTED
Transparent sym_eq.
*)
(* UNEXPORTED
Transparent f_equal.
*)
(* NOTATION
Notation Pair := (pair (B:=_)).
*)
(* NOTATION
Notation Proj1 := (proj1 (B:=_)).
*)
(* NOTATION
Notation Proj2 := (proj2 (B:=_)).
*)
(* Following only needed in finite, but tha's now obsolete
Lemma deMorgan_or_and: (A,B,X:Prop)((A\/B)->X)->(A->X)/\(B->X).
Tauto.
Qed.
Lemma deMorgan_and_or: (A,B,X:Prop)(A->X)/\(B->X)->(A\/B->X).
Tauto.
Qed.
Lemma deMorgan_ex_all:
(A:Set)(P:A->Prop)(X:Prop)((Ex P)->X)->(a:A)(P a)->X.
Intros. Apply H; Exists a; Assumption.
Qed.
Lemma deMorgan_all_ex:
(A:Set)(P:A->Prop)(X:Prop)((a:A)(P a)->X)->(Ex P)->X.
Intros. Elim H0; Assumption.
Qed.
Implicit Arguments Off.
Three lemmas for proving properties about definitions made with case
distinction to a sumbool, i.e. [{A} + {B}].
Lemma sumbool_rec_or : (A,B:Prop)(S:Set)(l,r:S)(s:{A}+{B})
(sumbool_rec A B [_:{A}+{B}]S [x:A]l [x:B]r s) = l \/
(sumbool_rec A B [_:{A}+{B}]S [x:A]l [x:B]r s) = r.
Intros. Elim s.
Intros. Left. Reflexivity.
Intros. Right. Reflexivity.
Qed.
*)
inline procedural "cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con" as lemma.
(* begin hide *)
(* UNEXPORTED
Set Implicit Arguments.
*)
(* UNEXPORTED
Unset Strict Implicit.
*)
(* end hide *)
(*#* **Some results about [Z]
We consider the injection [inject_nat] from [nat] to [Z] as a
coercion. *)
(* begin hide *)
(* COERCION
cic:/Coq/ZArith/BinInt/Z_of_nat.con
*)
(* end hide *)
inline procedural "cic:/CoRN/algebra/Basics/POS_anti_convert.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/NEG_anti_convert.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/convert_is_POS.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/min_convert_is_NEG.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/inject_nat_convert.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/Z_exh.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/nats_Z_ind.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con" as lemma.
(* begin hide *)
(* UNEXPORTED
Set Implicit Arguments.
*)
(* UNEXPORTED
Unset Strict Implicit.
*)
(* end hide *)
inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff.con" as definition.
(* begin hide *)
(* UNEXPORTED
Set Strict Implicit.
*)
(* UNEXPORTED
Unset Implicit Arguments.
*)
(* end hide *)
inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_O.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/proper_caseZ_diff.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/diff_Z_ind.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/Zlt_opp.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/Zgt_not_eq.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/Zmult_absorb.con" as lemma.
(* UNEXPORTED
Section Well_foundedT
*)
(* UNEXPORTED
cic:/CoRN/algebra/Basics/Well_foundedT/A.var
*)
(* UNEXPORTED
cic:/CoRN/algebra/Basics/Well_foundedT/R.var
*)
(*#* The accessibility predicate is defined to be non-informative *)
inline procedural "cic:/CoRN/algebra/Basics/Acc.ind".
(* UNEXPORTED
End Well_foundedT
*)
(* UNEXPORTED
Section AccT
*)
(* UNEXPORTED
cic:/CoRN/algebra/Basics/AccT/A.var
*)
inline procedural "cic:/CoRN/algebra/Basics/well_founded.con" as definition.
(* UNEXPORTED
End AccT
*)
(* UNEXPORTED
Implicit Arguments Acc [A].
*)
(* UNEXPORTED
Section IndT
*)
(* UNEXPORTED
cic:/CoRN/algebra/Basics/IndT/A.var
*)
(* UNEXPORTED
cic:/CoRN/algebra/Basics/IndT/R.var
*)
(* UNEXPORTED
Section AccIter
*)
(* UNEXPORTED
cic:/CoRN/algebra/Basics/IndT/AccIter/P.var
*)
(* UNEXPORTED
cic:/CoRN/algebra/Basics/IndT/AccIter/F.var
*)
inline procedural "cic:/CoRN/algebra/Basics/Acc_inv.con" as lemma.
inline procedural "cic:/CoRN/algebra/Basics/Acc_iter.con" as definition.
(* UNEXPORTED
End AccIter
*)
(* UNEXPORTED
cic:/CoRN/algebra/Basics/IndT/Rwf.var
*)
inline procedural "cic:/CoRN/algebra/Basics/well_founded_induction_type.con" as theorem.
(* UNEXPORTED
End IndT
*)
(* UNEXPORTED
Section InductionT
*)
(* UNEXPORTED
cic:/CoRN/algebra/Basics/InductionT/A.var
*)
(* UNEXPORTED
cic:/CoRN/algebra/Basics/InductionT/f.var
*)
inline procedural "cic:/CoRN/algebra/Basics/ltof.con" as definition.
inline procedural "cic:/CoRN/algebra/Basics/well_founded_ltof.con" as theorem.
inline procedural "cic:/CoRN/algebra/Basics/induction_ltof2T.con" as theorem.
(* UNEXPORTED
End InductionT
*)
(* UNEXPORTED
Section InductionTT
*)
inline procedural "cic:/CoRN/algebra/Basics/lt_wf_rect.con" as lemma.
(* UNEXPORTED
End InductionTT
*)