Library hurry

Check fun x => x*x.

Check fun a b c d e => a+b+c+d+e.

Definition sum5 := fun a b c d e => a+b+c+d+e.

Eval compute in sum5 1 2 3 4 5.


Definition is_zero (n:nat) :=
match n with
0 => true
| S p => false
end.

Eval compute in is_zero 5.
Eval compute in is_zero 0.

Print pred.

Fixpoint sum_n n :=
match n with
0 => 0
| S p => p + sum_n p
end.

Eval compute in sum_n 4.


Fixpoint sum_n2 n s :=
match n with
0 => s
| S p => sum_n2 p (p+s)
end.

Eval compute in sum_n2 5 5.

Fixpoint evenb n :=
match n with
0 => true
| 1 => false
| S (S p) => evenb p
end.

Eval compute in evenb 5.
Eval compute in evenb 8.

Search True.
Search le.
SearchPattern (_ + _ <= _ + _).
SearchAbout S.

Lemma example2 : forall a b:Prop, a /\ b -> b/\a.

Print example2.

Lemma example3 : forall A B, A \/B-> B\/A.

Print example3.

Check le_n.
Check le_S.
Lemma example4 : 3<=5.
Print example4.

Lemma example4b : forall n, n <= S (S n).
Print example4b.

Lemma example4c : 3<=5.
Print example4.
Print example4c.

Require Import Arith.
Check le_trans.

Lemma example5 : forall x y,
x<= 10 -> 10 <= y -> x<=y.

Print example5.

Lemma example6 : forall x y, (x +y) * (x+y)
= x*x +2*x*y +y*y.
SearchRewrite (_ * (_+_)).
SearchRewrite ((_+_)*_).
SearchRewrite (_+(_+_)).
SearchPattern (?x*?y=?y*?x).
SearchRewrite (S _*_).
Check mult_succ_l.
SearchRewrite (_*(_*_)).
Qed.
Print example6.

Require Import Omega.
Lemma omega_example:
 forall f x y, 0<x -> 0<f x ->
3* f x <= 2*y -> f x <= y.

Lemma exercise3_5_1 : forall A B C:Prop,
A/\(B/\C)->(A/\B)/\C.

Lemma exercise3_5_2 : forall A B C D:Prop,
(A->B)/\(C->D)/\A/\C -> B/\D.

Lemma exercise3_5_3 : forall A:Prop,
~(A/\~A).
SearchPattern (?A\/~?A).
Qed.

Lemma exercise3_5_4 : forall A B C: Prop,
A\/(B\/C)->(A\/B)\/C.

Lemma exercise3_5_5 : forall A B:Prop,
(A\/B)/\~A ->B.

Lemma exercise3_5_6 : forall A:Type,
forall P Q: A->Prop,
(forall x, P x)\/(forall y, Q y)->
forall x, P x\/ Q x.


Print sum_n.

Lemma sum_n_p : forall n,
2*sum_n n +n=n*n.

Print evenb.
Lemma evenb_p : forall n,
evenb n = true -> exists x, n=2*x.

Fixpoint add n m := match n with
0 => m
| S p => add p (S m)
end.

Lemma exercise4_1 : forall n m,
add n (S m) = S (add n m).

Lemma exercise4_2 : forall n m,
add (S n) m = S (add n m).

Lemma exercise4_3 : forall n m, add n m=n+m.

Fixpoint sum_odd_n (n:nat) : nat :=
match n with
0=>0
|S p=>1+2*p+sum_odd_n p
end.

Lemma exercise4_4 : forall n:nat,
sum_odd_n n=n*n.



Inductive bin : Type :=
L : bin
| N :bin -> bin -> bin.

Check L.
Check N L (N L L).

Inductive exercise6_1 :Type :=
CTE : exercise6_1
| TRH : nat -> exercise6_1 -> exercise6_1->exercise6_1
| FRH : bool ->exercise6_1->exercise6_1->exercise6_1->exercise6_1.
Check CTE.
Check TRH 5 CTE CTE.
Check FRH true CTE (TRH 3 CTE CTE) CTE.

Definition example7 ( t: bin):bool :=
match t with
N L L => false
| _ => true
end.

Fixpoint flatten_aux (t1 t2:bin):bin :=
match t1 with
L => N L t2
|N t'1 t'2 => flatten_aux t'1 (flatten_aux t'2 t2)
end.

Fixpoint flatten (t:bin):bin :=
match t with
L=>L
| N t1 t2 => flatten_aux t1 (flatten t2)
end.

Fixpoint size (t:bin):nat :=
match t with
L=> 1
|N t1 t2 => 1+size t1 +size t2
end.

Eval compute in flatten_aux(N L L) L.
Eval compute in flatten
 (N (N L L) (N L L)).

Print example7.
Lemma example7_size: forall t,
example7 t=false -> size t=3.

Lemma flatten_aux_size: forall t1 t2,
size (flatten_aux t1 t2) = size t1 +size t2 +1.

Lemma flatten_size : forall t,
size (flatten t) = size t.

Lemma not_subterm_self_1 : forall x y,
~x=N x y.

Print nat.
Eval compute in 3-7.
Eval compute in S(S(S(3))).

Fixpoint nat_fact(n:nat) : nat:=
match n with
0=>1
| S p=> S p * nat_fact p
end.

Fixpoint fib (n:nat) : nat :=
match n with
0=>0
|S q =>
 match q with
 0=>1
 | S p => fib p + fib q
 end
end.
Eval compute in fib 5.

Open Scope Z_scope.
Print iter.

Definition fact_aux(n:Z):=
iter n (Z*Z) (fun p=>(fst p+1,
 snd p * (fst p+1))) (0,1).
Definition Z_fact(n:Z):=snd(fact_aux n).

Close Scope Z_scope.

Inductive even : nat -> Prop :=
even0 : even 0
|evenS : forall x:nat, even x -> even (S (S x )).

Lemma even_mult : forall x, even x->
exists y, x=2*y.

Lemma not_even_1 : ~even 1.

Lemma even_inv : forall x, even(S(S x))->even x.