Require Import NaturalDeduction.
Require Import Hoare.
Require Import Lemmas.
Require Import Factorial.

(*
Question 1:
Prove the lemma below using the natural deduction rules of the class. 
*)

Lemma Q1 (A : Type) (P Q : A -> Prop) : (exists x, P x \/ Q x) /\ (forall x, P x -> Q x) -> (exists x, Q x).
Proof.
Admitted.

(*
Question 2:
Prove Lemma Q2. The function fact is the factorial function.
*)

Lemma Q2 (n i r : nat) :
{{ True }}
  i ::= 0;;  
  r ::= 1;;
  While negb (i =? n) 
  Do
    i ::= 1 + i;;
    r ::= i * r
  Od
{{ r = fact n }}.
Proof.
Admitted.

(*
Question 3:
Prove the following lemma. The lemmas f_equal, map_rev and rev_involutive might be useful.
*)

Definition factEach := map fact.

Lemma Q3 (p q r : Ptr) (l : list nat) :
{{ p implements l }}
  q ::= p;;
  r ::= Null;;
  While negb (q =p Null)
  Do
    r ::= new (fact (q^.elem)) r;;
    q ::= q^.next
  Od
{{ r implements rev (map fact l) }}.
Proof.
Admitted.