@ FII

Laborator - Polimorfism. Funcții de ordin superior. Demonstrații.

Demonstrați următoarele teoreme:

Theorem and_elim_1:
  forall (A B : Prop), A /\ B -> A.
Admitted.

Theorem and_elim_2:
  forall (A B : Prop), A /\ B -> B.
Admitted.

Theorem and_intro:
  forall (A B : Prop), A -> B -> (A /\ B).
Admitted.

Theorem or_elim:
  forall (A B C: Prop), (A -> C) -> (B -> C) -> (A \/ B) -> C.
Proof.
Admitted.

Theorem or_intro_1:
  forall (A B : Prop), A -> (A \/ B).
Proof.
Admitted.

Theorem or_intro_2:
  forall (A B : Prop), B -> (A \/ B).
Proof.
Admitted.

Theorem not_not:
  forall (P : Prop), P -> ~~P.
Proof.
Admitted.

Theorem mp :
  forall A B,
    (A -> B) -> A -> B.
Proof.
Admitted.

Theorem mt :
  forall (A B : Prop),
    (A -> B) -> ~ B -> ~ A.
Proof.

(1 punct) Definiți un tip de date polimorfic pentru arbori binari.
(0.5 puncte) Definiți o funcție size care calculează numărul de noduri al un arbore binar (al cărui tip a fost definit la exercițiul 1) dat ca parametru. Pentru valoarea de return folosiți tipul nat din Coq (detalii AICI).
(0.5 puncte) Definiți o funcție height care calculează înățimea unui arbore binar (al cărui tip a fost definit la exercițiul 1) dat ca parametru. Pentru valoarea de return folosiți tipul nat din Coq.
(1 punct) Demonstrați că valoarea returnată de funcția height este mai mică sau egală decât valoarea returnată de funcția size.
(3 puncte) Scrieți o funcție de nivel superior denumită flatten care primește un arbore binar parametric în tipul T și o funcție f de tip T -> T și returnează o listă de tipul list T. Această listă conține elementele arborelui corespunzătoare parcurgerii preordine, peste care s-a aplicat funcția f. Detalii despre tipul parametric list sunt disponibile AICI.