Require Import NaturalDeduction.

Require Import PeanoNat.
Import Nat.
Require Import List.
Import ListNotations.

(* In order to print a lemma from the library you can use Check, e.g. Check or_assoc. *)

Lemma L1 (A : Type) : forall (l1 l2 : list A) (a : A), In a l1 \/ In a l2 -> In a (l1 ++ l2).
(* The lemma or_assoc might be helpful. No other lemma is needed. *)
Proof.
induction l1.
simpl.
Forall_Intro.
Forall_Intro.
Impl_Intro.
Or_Elim in H.
PBC.
assumption.
assumption.
simpl.
Forall_Intro.
Forall_Intro.
Impl_Intro.
Or_Elim in H.
Or_Elim in H.
Or_Intro_1.
assumption.
Or_Intro_2.
apply IHl1.
Or_Intro_1.
assumption.
Or_Intro_2.
apply IHl1.
Or_Intro_2.
assumption.
Qed.

Lemma L2 (A : Type) : forall (l : list A), length (rev l) = length l.
(* The lemmas app_length and add_1_r might be helpful. No other lemma is needed. *)
Proof.
induction l.
simpl.
trivial.
simpl.
rewrite app_length.
simpl.
rewrite IHl.
rewrite add_1_r.
trivial.
Qed.

Lemma L3 (A B : Type) : forall (l : list A) (f : A -> B) (x : A), In x l -> In (f x) (map f l).
(* map is the function that applies a function f to each element of a list l. *)
(* The lemmas in_inv and f_equal might be helpful. No other lemma is needed. *)
Proof.
induction l.
Forall_Intro.
Forall_Intro.
simpl.
Impl_Intro.
assumption.
simpl.
Forall_Intro.
Forall_Intro.
Impl_Intro.
Or_Elim in H.
Or_Intro_1.
apply f_equal.
assumption.
Or_Intro_2.
apply IHl.
assumption.
Qed.

Lemma L4 (r n : nat) :
{{ 1 <= n }}
  r ::= 1;;
  While (negb (r =? n)) 
  Do
    r ::= 2*r
  Od
{{ exists i, 2^i = n }}.
Proof.
Hoare_while_tactic with (exists i, 2^i = r).
(* Prop 1 *)
Impl_Intro.
Exists_Intro with 0.
simpl.
trivial.
(* Prop 2 *)
Impl_Intro.
And_Elim_1 in H.
Exists_Elim in H0.
Exists_Intro with (S x).
simpl.
rewrite H1.
trivial.
(* Prop 3 *)
Impl_Intro.
And_Elim_all in H.
bool2Prop in H0.
rewrite H0 in H.
assumption.
Qed.

Lemma L4_alternative (r n : nat) :
{{ 1 <= n }}
  r ::= 1;;
  While (negb (r =? n)) 
  Do
    r ::= 2*r
  Od
{{ exists i, 2^i = n }}.
Proof.
Hoare_sequence_rule with (exists i, 2^i = r).
Hoare_consequence_rule_left with (exists i, 2^i = 1).
Impl_Intro.
Exists_Intro with 0.
simpl.
trivial.
Hoare_assignment_rule.
Hoare_consequence_rule_right with ((exists i, 2^i = r) /\ negb (r =? n) = false).
Hoare_while_rule.
Hoare_consequence_rule_left with (exists i, 2^i = 2*r).
Impl_Intro.
And_Elim_1 in H.
Exists_Elim in H0.
Exists_Intro with (S x).
simpl.
rewrite H1.
trivial.
Hoare_assignment_rule.
Impl_Intro.
And_Elim_all in H.
bool2Prop in H0.
rewrite H0 in H.
assumption.
Qed.

Lemma L5help (m n : nat) : m <= n -> n <= m -> m = n.
(* Proof this lemma first. There is no induction needed but the lemmas Lt.le_lt_or_eq and Lt.le_not_lt might be helpful. *)
Proof.
Impl_Intro.
Impl_Intro.
apply Lt.le_lt_or_eq in H.
Or_Elim in H.
apply Lt.le_not_lt in H0.
Not_Elim in H0 and H.
PBC.
assumption.
trivial.
Qed.

Lemma L5 (r m n : nat) :
{{ True }}
  r ::= 0;;
  While ((r<?m) && (r<?n))
  Do
    r ::= r+1
  Od
{{ min m n = r }}. 
(* The lemmas L5help (above), le_0_n, add_1_r, Lt.lt_le_S, nlt_ge, min_l and min_r might be helpful. No other lemma is needed. *)
Proof.
Hoare_while_tactic with (r <= m /\ r <= n).
(* Prop 1 *)
Impl_Intro.
And_Intro.
apply le_0_n.
apply le_0_n.
(* Prop 2 *)
Impl_Intro.
And_Intro.
And_Elim_2 in H.
bool2Prop in H0.
And_Elim_1 in H0.
rewrite add_1_r.
apply Lt.lt_le_S.
assumption.
And_Elim_2 in H.
bool2Prop in H0.
And_Elim_2 in H0.
rewrite add_1_r.
apply Lt.lt_le_S.
assumption.
(* Prop 3 *)
Impl_Intro.
bool2Prop in H.
simpl.
And_Elim_all in H.
Or_Elim in H0.
apply nlt_ge in H0.
assert (H2 := L5help _ _ H H0).
rewrite H2.
rewrite H2 in H1.
apply min_l.
assumption.
apply nlt_ge in H0.
assert (H2 := L5help _ _ H1 H0).
rewrite H2.
rewrite H2 in H.
apply min_r.
assumption.
Qed.