binders referenced! Fixed.
set "baseuri" "cic:/matita/Z/".
set "baseuri" "cic:/matita/Z/".
-include "../nat/nat.ma".
+include "nat/nat.ma".
+include "datatypes/bool.ma".
inductive Z : Set \def
OZ : Z
inductive Z : Set \def
OZ : Z
(* *)
(**************************************************************************)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/compare.ma".
+set "baseuri" "cic:/matita/nat/compare".
include "nat/orders.ma".
include "datatypes/bool.ma".
include "nat/orders.ma".
include "datatypes/bool.ma".
(* *)
(**************************************************************************)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/minus.ma".
+set "baseuri" "cic:/matita/nat/minus".
include "nat/orders_op.ma".
include "nat/times.ma".
include "nat/orders_op.ma".
include "nat/times.ma".
(* *)
(**************************************************************************)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/orders.ma".
+set "baseuri" "cic:/matita/nat/orders".
include "logic/connectives.ma".
include "logic/equality.ma".
include "logic/connectives.ma".
include "logic/equality.ma".
theorem le_S_S_to_le : \forall n,m:nat. le (S n) (S m) \to le n m.
intros.change with le (pred (S n)) (pred (S m)).
theorem le_S_S_to_le : \forall n,m:nat. le (S n) (S m) \to le n m.
intros.change with le (pred (S n)) (pred (S m)).
-elim H.apply le_n.apply trans_le ? (pred x).assumption.
+elim H.apply le_n.apply trans_le ? (pred e2).assumption.
(* *)
(**************************************************************************)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/orders_op.ma".
+set "baseuri" "cic:/matita/nat/orders_op".
include "higher_order_defs/functions.ma".
include "nat/times.ma".
include "higher_order_defs/functions.ma".
include "nat/times.ma".
(* *)
(**************************************************************************)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/plus.ma".
+set "baseuri" "cic:/matita/nat/plus".
include "logic/equality.ma".
include "nat/nat.ma".
include "logic/equality.ma".
include "nat/nat.ma".
qed.
theorem inj_plus_l: \forall p,n,m:nat.eq nat (plus n p) (plus m p) \to (eq nat n m)
qed.
theorem inj_plus_l: \forall p,n,m:nat.eq nat (plus n p) (plus m p) \to (eq nat n m)
-\def injective_plus_l.
\ No newline at end of file
(* *)
(**************************************************************************)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/times.ma".
+set "baseuri" "cic:/matita/nat/times".
include "logic/equality.ma".
include "nat/nat.ma".
include "logic/equality.ma".
include "nat/nat.ma".
theorem le_gen_x_O_aux: \forall x, y. (le x y) \to (y =O) \to
(x = O).
theorem le_gen_x_O_aux: \forall x, y. (le x y) \to (y =O) \to
(x = O).
-intros 3. elim H. auto. apply eq_gen_S_O. exact x2. auto.
+intros 3. elim H. auto. apply eq_gen_S_O. exact e3. auto.
qed.
theorem le_gen_x_O: \forall x. (le x O) \to (x = O).
qed.
theorem le_gen_x_O: \forall x. (le x O) \to (x = O).
(\exists n. x = (S n) \land (le m n)).
intros 4. elim H.
apply eq_gen_S_O. exact m. elim H1. auto.
(\exists n. x = (S n) \land (le m n)).
intros 4. elim H.
apply eq_gen_S_O. exact m. elim H1. auto.
-cut x1 = m. elim Hcut. apply ex_intro. exact x2. auto. auto.
+cut e4 = m. elim Hcut. apply ex_intro. exact e3. auto. auto.
qed.
theorem le_gen_S_x: \forall m,x. (le (S m) x) \to
qed.
theorem le_gen_S_x: \forall m,x. (le (S m) x) \to
-let fresh_binder =
- function
- | true ->
- incr counter;
- Cic.Name ("e" ^ string_of_int !counter)
- | _ -> Cic.Anonymous
+let fresh_binder () =
+ incr counter;
+ Cic.Name ("e" ^ string_of_int !counter)
(** verifies if a given inductive type occurs in a term in target position *)
let rec recursive uri typeno = function
(** verifies if a given inductive type occurs in a term in target position *)
let rec recursive uri typeno = function
(CicSubstitution.lift 1 p) [Cic.Rel 1]
in
let tgt = CicSubstitution.lift 1 tgt in
(CicSubstitution.lift 1 p) [Cic.Rel 1]
in
let tgt = CicSubstitution.lift 1 tgt in
- Cic.Prod (fresh_binder dependent, src,
+ Cic.Prod (fresh_binder (), src,
Cic.Prod (Cic.Anonymous, phi,
delta (uri, typeno) dependent paramsno consno tgt
(CicSubstitution.lift 2 p) (args @ [Cic.Rel 2])))
else (* non recursive *)
let args = List.map (CicSubstitution.lift 1) args in
Cic.Prod (Cic.Anonymous, phi,
delta (uri, typeno) dependent paramsno consno tgt
(CicSubstitution.lift 2 p) (args @ [Cic.Rel 2])))
else (* non recursive *)
let args = List.map (CicSubstitution.lift 1) args in
- Cic.Prod (fresh_binder dependent, src,
+ Cic.Prod (fresh_binder (), src,
delta (uri, typeno) dependent paramsno consno tgt
(CicSubstitution.lift 1 p) (args @ [Cic.Rel 1]))
| _ -> assert false
delta (uri, typeno) dependent paramsno consno tgt
(CicSubstitution.lift 1 p) (args @ [Cic.Rel 1]))
| _ -> assert false
else
match ty with
| Cic.Prod (name, src, tgt) ->
else
match ty with
| Cic.Prod (name, src, tgt) ->
+ let name =
+ match name with
+ Cic.Name _ -> name
+ | Cic.Anonymous -> fresh_binder ()
+ in
binder name src (add_params binder (indno - 1) tgt eliminator)
| _ -> assert false
binder name src (add_params binder (indno - 1) tgt eliminator)
| _ -> assert false
let rec type_of_p sort dependent leftno indty = function
| Cic.Prod (n, src, tgt) when leftno = 0 ->
let rec type_of_p sort dependent leftno indty = function
| Cic.Prod (n, src, tgt) when leftno = 0 ->
- Cic.Prod (n, src, type_of_p sort dependent leftno indty tgt)
+ let n =
+ if dependent then
+ match n with
+ Cic.Name _ -> n
+ | Cic.Anonymous -> fresh_binder ()
+ else
+ n
+ in
+ Cic.Prod (n, src, type_of_p sort dependent leftno indty tgt)
| Cic.Prod (_, _, tgt) -> type_of_p sort dependent (leftno - 1) indty tgt
| t ->
if dependent then
| Cic.Prod (_, _, tgt) -> type_of_p sort dependent (leftno - 1) indty tgt
| t ->
if dependent then
let rec add_right_pi dependent strip liftno liftfrom rightno indty = function
| Cic.Prod (_, src, tgt) when strip = 0 ->
let rec add_right_pi dependent strip liftno liftfrom rightno indty = function
| Cic.Prod (_, src, tgt) when strip = 0 ->
- Cic.Prod (fresh_binder true,
+ Cic.Prod (fresh_binder (),
CicSubstitution.lift_from liftfrom liftno src,
add_right_pi dependent strip liftno (liftfrom + 1) rightno indty tgt)
| Cic.Prod (_, _, tgt) ->
add_right_pi dependent (strip - 1) liftno liftfrom rightno indty tgt
| t ->
if dependent then
CicSubstitution.lift_from liftfrom liftno src,
add_right_pi dependent strip liftno (liftfrom + 1) rightno indty tgt)
| Cic.Prod (_, _, tgt) ->
add_right_pi dependent (strip - 1) liftno liftfrom rightno indty tgt
| t ->
if dependent then
- Cic.Prod (fresh_binder dependent,
+ Cic.Prod (fresh_binder (),
CicSubstitution.lift_from (rightno + 1) liftno indty,
Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 0 (rightno + 1)))
else
CicSubstitution.lift_from (rightno + 1) liftno indty,
Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 0 (rightno + 1)))
else
let rec add_right_lambda dependent strip liftno liftfrom rightno indty case =
function
| Cic.Prod (_, src, tgt) when strip = 0 ->
let rec add_right_lambda dependent strip liftno liftfrom rightno indty case =
function
| Cic.Prod (_, src, tgt) when strip = 0 ->
- Cic.Lambda (fresh_binder true,
+ Cic.Lambda (fresh_binder (),
CicSubstitution.lift_from liftfrom liftno src,
add_right_lambda dependent strip liftno (liftfrom + 1) rightno indty
case tgt)
| Cic.Prod (_, _, tgt) ->
CicSubstitution.lift_from liftfrom liftno src,
add_right_lambda dependent strip liftno (liftfrom + 1) rightno indty
case tgt)
| Cic.Prod (_, _, tgt) ->
- add_right_lambda dependent (strip - 1) liftno liftfrom rightno indty
+ add_right_lambda true (strip - 1) liftno liftfrom rightno indty
- Cic.Lambda (fresh_binder true,
+ Cic.Lambda (fresh_binder (),
CicSubstitution.lift_from (rightno + 1) liftno indty, case)
let rec branch (uri, typeno) insource paramsno t fix head args =
CicSubstitution.lift_from (rightno + 1) liftno indty, case)
let rec branch (uri, typeno) insource paramsno t fix head args =
let src = CicSubstitution.lift 1 src in
branch (uri, typeno) true paramsno src fix head [Cic.Rel 1]
in
let src = CicSubstitution.lift 1 src in
branch (uri, typeno) true paramsno src fix head [Cic.Rel 1]
in
- Cic.Lambda (fresh_binder true, src,
+ Cic.Lambda (fresh_binder (), src,
branch (uri, typeno) insource paramsno tgt
(CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
(args @ [Cic.Rel 1; phi]))
else (* non recursive *)
let args = List.map (CicSubstitution.lift 1) args in
branch (uri, typeno) insource paramsno tgt
(CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
(args @ [Cic.Rel 1; phi]))
else (* non recursive *)
let args = List.map (CicSubstitution.lift 1) args in
- Cic.Lambda (fresh_binder true, src,
+ Cic.Lambda (fresh_binder (), src,
branch (uri, typeno) insource paramsno tgt
(CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
(args @ [Cic.Rel 1]))
branch (uri, typeno) insource paramsno tgt
(CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
(args @ [Cic.Rel 1]))
(fun (_, constructor) acc ->
decr consno;
let p = Cic.Rel !consno in
(fun (_, constructor) acc ->
decr consno;
let p = Cic.Rel !consno in
- Cic.Lambda (fresh_binder true,
+ Cic.Lambda (fresh_binder (),
(delta (uri, typeno) dependent leftno !consno
constructor p [mk_constructor !consno]),
acc))
(delta (uri, typeno) dependent leftno !consno
constructor p [mk_constructor !consno]),
acc))