(* NOMBRE COMPLETO *)

Require Import List.

Section Problema1.

Definition and (b1 b2 : bool) :=
    match b2 with
        | true => b1
        | false => false
    end.

Fixpoint append (A:Set) (l1 l2 : list A) : list A :=
    match l1 with
        | nil => l2
        | cons x xs => cons x (append A xs l2)
    end.

Fixpoint forAll (A:Set) (p: A -> bool) (l : list A) : bool :=
     match l with
         | nil => true
         | cons x xs => if (p x) then forAll A p xs else false
     end.

Lemma Ej11 : forall (A : Set) (l1 l2 : list A) (p : A -> bool), forAll A p (append A l1 l2) = and (forAll A p l2) (forAll A p l1).
Proof.  
    induction l1; simpl; intros.
    reflexivity.
    elim (p a); auto.    
Qed.

Lemma Ej12 : forall (A : Set) (l1 l2 : list A) (p : A -> bool), forAll A p l2 = true -> forAll A p (append A l1 l2) = forAll A p l1.
Proof.
    intros.
    rewrite Ej11.
    rewrite H.
    elim (forAll A p l1); auto.
Qed.
 
Lemma Ej13 : forall (A : Set) (l : list A) (p : A -> bool), forAll A p l = false -> l <> nil.
Proof.
     unfold not; intros.
     rewrite H0 in H.
     inversion H.
Qed.

End Problema1.


Section Problema2.

Require Import Lia.

Inductive sorted : list nat -> Prop :=
    | sortedNil : sorted nil
    | sortedOne : forall (x:nat), sorted (cons x nil)
    | sortedCons : forall (l : list nat) (x y:nat), sorted (cons y l) -> x > y -> 
	sorted (cons x (cons y l)).

Inductive noRep : list nat -> Prop :=
    | noRepNil : noRep nil
    | noRepOne : forall (x:nat), noRep (cons x nil)
    | noRepCons : forall (l : list nat) (x y:nat), noRep (cons y l) -> x <> y -> noRep (cons x (cons y l)).

Hint Constructors sorted noRep.

Lemma Ej21 : forall (l : list nat), sorted l -> noRep l.
	intros l sortedl; elim sortedl; auto.
	intros.
	apply noRepCons; [auto | lia].
Qed.

Lemma Ej22 : forall (x:nat) (l : list nat), sorted (cons x l) -> sorted l.
destruct l; simpl; intros; auto.
inversion_clear H; assumption.
Qed.

Lemma Ej23: forall (l1 l2:list nat), sorted (append nat l1 l2) -> sorted l1 /\ sorted l2.
Proof.
	induction l1; simpl; intros; split; auto.
	generalize IHl1 H; destruct l1; simpl; intros; auto.
	constructor; inversion_clear H; auto.
	elim (IHl1 l2 H1); auto. 
	elim (IHl1 l2 (Ej22 a (append nat l1 l2) H)); auto.
Qed.

End Problema2.


Section Problema3.

Variable A: Set.

Set Implicit Arguments. (* Puede quitar esta línea si lo prefiere *) 

Inductive tree : Set :=
| leaf : tree 
| node : A -> tree -> tree -> tree.

Fixpoint size (t : tree) {struct t} : nat :=
    match t with
        | leaf => 0
        | node _ t1 t2  => (size t1) + 1 + (size t2)
    end.

Require Import Inverse_Image.
Require Import Wf_nat.

Definition tree_lt (t1 t2 : tree) := size t1 < size t2.

Lemma L3 : well_founded tree_lt.
Proof.
  unfold tree_lt.
  apply wf_inverse_image.
	apply lt_wf.
Qed.

End Problema3.