Coq

Theorem plus0:
  forall n : nat , 0 + n = n.
Proof.
  intro x. (* becomes 0 + x = x *)
  compute.
  reflexivity.
Qed.

Variables P Q R : Prop.
Hypothesis H : P -> Q -> R.
Lemma l : P /\ Q -> R.
Proof.
  intro.
  apply H. (* Two goals: P, Q. The 1st goal: P *)
  destruct H0.
  assumption. (* The next goal: Q, same steps *)
  destruct H0.
  assumption.
Qed.

(* Alternatively, destruct H0; assumption *)
Lemma l1 : P /\ Q -> R.
Proof.
  intros.
  destruct H0.
  apply H ; assumption.
Qed.

Theorem th4:
  forall b: bool, negb (negb b) = b.
Proof.
  intros.
  destruct b eqn:E.
  reflexivity. ()
  reflexivity.
Qed.

Theorem th3:
  forall n: nat, (n+1 =? 0) = false.
Proof.
  intros.
  destruct n as [ | n'] eqn:E.
  compute. (* E : n = 0, goal : (0 + 1 =? 0) = false *)
  reflexivity.
  compute. (* E : n = S n', goal : (S n' + 1 =? 0) = false *)
  reflexivity.
Qed.

Theorem th5:
  forall b c: bool, andb b c = andb c b. (* auto detect types for b, c *)
Proof.
  intros.
  destruct b eqn:Eb.   (* destruct b; desctruct c; reflexivity, on every subtree do destruct c, reflexivity *)
  destruct c eqn:Ec.
  reflexivity.
  reflexivity.
  destruct c.
  reflexivity.
  reflexivity.
Qed.

Theorem S_injective' :
  forall n m : nat,
    S n = S m -> n = m.
Proof.
  intros n m H. (* H: S n = S m *)
  injection H as H0. (* H0: n = m *)
  apply H0.
Qed.

Inductive rgb : Type :=
| red
| green
| blue.

Check red. (* white : color *)

Inductive color : Type :=
| white
| black
| primary (p: rgb).

Check primary. (* primary : rgb -> color *)
Check primary red. (* primary : color *)

Inductive natprod : Type :=
| pair (n1 n2 : nat).

Definition fst (p: natprod) : nat :=
  match p with
  | pair x _ => x
  end.

Definition snd (p: natprod) : nat :=
  match p with
  | pair _ y => y
  end.

Definition swap_pair (p: natprod) : natprod :=
  match p with
  | (x, y) => (y, x)
  end.

Notation "( x , y )" := (pair x y).

Inductive natlist : Type :=
| nil
| cons (n : nat) (l : natlist).
(* cons stands for "constructor". It's just a name *)
(* n represent the beginning item, l represent the tail of the list *)

Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

  Fixpoint repeat(n count: nat) : natlist :=
    match count with
    | 0 => []
    | S count' => n :: (repeat n count')
    end.

  Fixpoint length(l: natlist) : nat :=
    match l with
    | [] => 0
    | _ :: l' => S (length l')
    end.

Fixpoint append(l1 l2: natlist) : natlist :=
  match l1 with
  | [] => l2
  | h :: t =>  h :: (append t l2)
  end.

Notation "x ++ y" := (append x y)
                     (right associativity, at level 60).

Definition hd (default: nat)(l: natlist) : nat :=
  match l with
  | [] => default
  | h :: _ => h
  end.

Definition tl (l: natlist) : natlist :=
  match l with
  | [] => []
  | _ :: t => t
  end.

Fixpoint last_element (default: nat)(l: natlist) : nat :=
  match l with
  | [] => default
  | n :: [] => n
  | n :: t => last_element default t
  end.

  Theorem tl_length_pred :
      forall lst: natlist,
        pred (length lst) = length (tl lst).
  Proof.
    intros.
    destruct lst as [ | h t].
    compute.
    reflexivity.
    simpl. (* pred (length (h :: t)) = length (tl (h :: t)) *)
    reflexivity.
  Qed.

Theorem app_assoc :
  forall lst1 lst2 lst3 : natlist,
    (lst1 ++ lst2) ++ lst3 = lst1 ++ (lst2 ++ lst3).
Proof.
  intros.
  induction lst1 as [ | h1 t1].
  simpl.
  reflexivity.
  simpl.
  rewrite IHt1.
  reflexivity.
Qed.

Theorem app_length :
  forall lst1 lst2 : natlist,
  length (lst1 ++ lst2) = (length lst1) + (length lst2).
Proof.
  intros.
  induction lst1 as [ | h1 t1].
  simpl.
  reflexivity.
  simpl.
  rewrite <- IHt1.
  reflexivity.
Qed.

Fixpoint rev (lst: natlist) : natlist :=
  match lst with
  | [] => []
  | h :: t => rev t ++ [h]
  end.

Theorem rev_length:
  forall lst: natlist,
  length (rev lst) = length lst.
Proof.
  intros.
  induction lst as [| h t].
  compute.
  reflexivity.
  simpl.
  rewrite app_length.
  simpl.
  rewrite IHt. (* length t + 1 = S (length t) *)
  rewrite nat_add_com. (* 1 + length t = S (length t) *)
  simpl.
  reflexivity.
Qed.

Fixpoint nth_bad (lst: natlist)(n : nat) : nat :=
  match lst with
  | [] => 420 (* any default value *)
  | h :: t =>
    match n with
    | 0 => h
    | S k => nth_bad t k
    end
  end.

Inductive natoption : Type :=
  | None
  | Some (n: nat).

Fixpoint nth_error (lst: natlist)(n:nat) : natoption :=
  match lst with
  | [] => None
  | h :: t =>
      match n with
      | 0 => Some h
      | S k => nth_error t k
      end
   end.

Module PartialMap.

Inductive partial_map : Type :=
  | Empty
  | Binding (k: nat)(v: nat)(m: partial_map).

Definition update(k : nat)(v: nat)(m: partial_map) : partial_map :=
  Binding k v m.

Fixpoint find(k: nat) (m: partial_map) : natoption :=
  match m with
  | Empty => None
  | Binding k2 v m' =>
      if k =? k2 then Some v else find k m'
  end.

Theorem find_update:
  forall (m: partial_map) (k v: nat),
    find k (update k v m) = Some v.
Proof.
  intros.
  simpl.
  rewrite eq_refl.
  reflexivity.
Qed.

Search rev. (* theorems whose name contains 'rev' *)
Search (_ + _ = _ + _).

Module Polymorphism.

(* Polymorphic Lists *)

Inductive list (X: Type) : Type :=
  | nil
  | cons (x: X)(l: list X).

Fixpoint repeat (X: Type)(x: X)(count: nat) : list X :=
  match count with
  | 0 => nil X
  | S count' => cons X x (repeat X x count')
  end.

Fixpoint repeat'' X x count : list X :=
  match count with
  | 0 => nil _
  | S count' => cons _ x (repeat'' _ x count')
  end.

Check cons _ 1 (cons _ 2 (cons _ 3 (nil _))). (* detect that _ should be nat *)

Arguments nil {X}.
Arguments cons {X}.
Arguments repeat {X}.

Check cons 1 (cons 2 (cons 3 nil)). (* : list nat *)

Fixpoint repeat''' {X: Type} (x: X) (count: nat) : list X :=
  match count with
  | 0 => nil
  | S count' => cons x (repeat''' x count')
  end.

Fixpoint app {X: Type}(l1 l2: list X) : list X :=
  match l1 with
  | nil => l2
  | cons h t => cons h (app t l2)
  end.

Fixpoint rev {X: Type}(l: list X) : list X :=
  match l with
  | nil => nil
  | cons h t => app (rev t)(cons h nil)
  end.

Fixpoint length {X: Type}(l : list X) : nat :=
  match l with
  | nil => 0
  | cons _ l' => S (length l')
  end.

Definition x : list nat := nil. (* not doable: Definition x := nil *)

Notation "x :: y" := (cons x y)
                     (at level 60, right associativity).

Notation "[ ]" := nil.

Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).

Notation "x ++ y" := (app x y)
                     (at level 60, right associativity).


Theorem app_assoc:
  forall X (lst1 lst2 lst3 : list X),
    lst1 ++ lst2 ++ lst3 = (lst1 ++ lst2) ++ lst3.
Proof.
  intros.
  induction lst1 as [| h1 t1].
  simpl.
  reflexivity.
  simpl.
  rewrite IHt1.
  reflexivity.
Qed.

Inductive prod (X Y: Type) : Type :=
  | pair (x: X)(y: Y).

Arguments pair {X}{Y}.

Notation "( x , y )" := (pair x y).

Notation "X * Y" := (prod X Y) : type_scope.

Fixpoint zip {X Y} (lx: list X)(ly: list Y) : list (X*Y) :=
  match lx, ly with
  | [], _ => []
  | _, [] => []
  | hx :: tx, hy :: ty => (hx, hy) :: (zip tx ty)
  end.

Compute zip [true;false] [3;4;5]. (* = [(true, 3); (false, 4)] : list (nat * nat)*)

Module PolyOption.

Inductive option (X : Type) : Type :=
  | Some (x: X)
  | None.

Arguments Some {X}.
Arguments None {X}.

End PolyOption.

Fixpoint nth_error {X}(l: list X)(n: nat) : option X :=
  match l with
  | [] => None
  | a :: l' => match n with
               | O => Some a
               | S n' => nth_error l' n'
               end
  end.

Definition simple_add (a b: nat) : nat :=
  a + b.

Check simple_add. (* : nat -> nat -> nat *)

Definition applythrice {X}(f: X -> X) (n: X) : X :=
  f(f (f n)).

Fixpoint filter {X}(test: X -> bool)(l: list X) : list X :=
  match l with
  | [] => []
  | h :: t =>
      if test h then h :: (filter test t)
      else filter test t
  end.

Definition countodd (l : list nat) : nat :=
  length (filter odd l).

Fixpoint map {X Y}(f: X->Y)(lst: list X) : list Y :=
  match lst with
  | [] => []
  | h :: t => (f h) :: (map f t)
  end.
Definition option_map {X Y}(f: X -> Y)(xo: option X) : option Y :=
match xo with
| None => None
| Some x => Some (f x)
end.

Fixpoint fold {X Y} (f: X -> Y -> Y) (lst: list X) (b: Y) : Y :=
  match lst with
  | [] => b
  | h :: t => f h (fold f t b)
  end.

Definition mysquare(n : nat) : nat :=
  n * n.
Check mysquare. (* : nat -> nat *)
Check (fun n => n * n). (* : nat -> nat *)
Compute (fun n => n * n) 2. (* 4 *)

Definition constfun {X}(x: X) : nat -> X :=
  fun (k: nat) => x.

Module RegExp.

Inductive reg_exp (T : Type) : Type :=
  | EmptySet
  | EmptyStr
  | Char (t : T)
  | App (r1 r2 : reg_exp T)
  | Union (r1 r2 : reg_exp T)
  | Star (r : reg_exp T).

Arguments EmptySet {T}.
Arguments EmptyStr {T}.
Arguments Char {T}.
Arguments App {T}.
Arguments Union {T}.
Arguments Star {T}.

Reserved Notation "s =~ re" (at level 80).

Inductive exp_match {T} : list T -> reg_exp T -> Prop :=
  | MEmpty : [] =~ EmptyStr
  | MChar x : [x] =~ (Char x)
  | MApp s1 re1 s2 re2
             (H1 : s1 =~ re1)
             (H2 : s2 =~ re2)
           : (s1 ++ s2) =~ (App re1 re2)
  | MUnionL s1 re1 re2
                (H1 : s1 =~ re1)
              : s1 =~ (Union re1 re2)
  | MUnionR re1 s2 re2
                (H2 : s2 =~ re2)
              : s2 =~ (Union re1 re2)
  | MStar0 re : [] =~ (Star re)
  | MStarApp s1 s2 re
                 (H1 : s1 =~ re)
                 (H2 : s2 =~ (Star re))
               : (s1 ++ s2) =~ (Star re)

  where "s =~ re" := (exp_match s re).

End RegExp.

Reserved Notation "e '==>' n" (at level 90, left associativity).

Inductive aexp : Type :=
| ANum (n : nat)
| APlus (a1 a2 : aexp)
| AMinus (a1 a2 : aexp)
| AMult (a1 a2 : aexp)
| ADiv (a1 a2 : aexp).

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum (n : nat) :
      (ANum n) ==> n
  | E_APlus (e1 e2 : aexp) (n1 n2 : nat) :
      (e1 ==> n1) ->
      (e2 ==> n2) ->
      (APlus e1 e2) ==> (n1 + n2)
  | E_AMinus (e1 e2 : aexp) (n1 n2 : nat) :
      (e1 ==> n1) ->
      (e2 ==> n2) ->
      (AMinus e1 e2) ==> (n1 - n2)
  | E_AMult (e1 e2 : aexp) (n1 n2 : nat) :
      (e1 ==> n1) ->
      (e2 ==> n2) ->
      (AMult e1 e2) ==> (n1 * n2)
  | E_ADiv (a1 a2 : aexp) (n1 n2 n3 n4 : nat) :
      (a1 ==> n1) -> (a2 ==> n2) -> (n2 > 0) ->
      (mult n2 n3 + n4 =? n1 = true) -> (n4 < n2) -> (ADiv a1 a2) ==> n3

  where "e '==>' n" := (aevalR e n) : type_scope.

Module States.

From Coq Require Import Arith.Arith.
From Coq Require Import Bool.Bool.
Require Export Coq.Strings.String.
From Coq Require Import Logic.FunctionalExtensionality.
From Coq Require Import Lists.List.
Import ListNotations.


Definition total_map (A : Type) := string -> A.

Definition t_empty {A: Type} (default : A) : total_map A := (fun _ => default).

Definition t_update {A: Type} (m: total_map A)(x: string)(v: A) :=
   fun x' => if eqb x x' then v else m x'.


Notation "x '!->' v ';' m" := (t_update m x v)
                              (at level 100, v at next level, right associativity).
Notation "x '!->' v" := (x !-> v ; t_empty 0) (at level 100).


Definition state := total_map nat.

Inductive aexp : Type :=
  | ANum (n : nat)

  | AId (x : string)

  | APlus (a1 a2 : aexp)
  | AMinus (a1 a2 : aexp)
  | AMult (a1 a2 : aexp).

Inductive bexp : Type :=
  | BTrue
  | BFalse
  | BEq (a1 a2 : aexp)
  | BNeq (a1 a2 : aexp)
  | BLe (a1 a2 : aexp)
  | BGt (a1 a2 : aexp)
  | BNot (b : bexp)
  | BAnd (b1 b2 : bexp).

Coercion AId : string >-> aexp.
Coercion ANum : nat >-> aexp.

Declare Custom Entry com.
Declare Scope com_scope.

Notation "<{ e }>" := e (at level 0, e custom com at level 99) : com_scope.

Notation "( x )" := x (in custom com, x at level 99) : com_scope.
Notation "x" := x (in custom com at level 0, x constr at level 0) : com_scope.
Notation "f x .. y" := (.. (f x) .. y)
                  (in custom com at level 0, only parsing,
                  f constr at level 0, x constr at level 9,
                  y constr at level 9) : com_scope.
Notation "x + y" := (APlus x y) (in custom com at level 50, left associativity).
Notation "x - y" := (AMinus x y) (in custom com at level 50, left associativity).
Notation "x * y" := (AMult x y) (in custom com at level 40, left associativity).
Notation "'true'" := true (at level 1).
Notation "'true'" := BTrue (in custom com at level 0).
Notation "'false'" := false (at level 1).
Notation "'false'" := BFalse (in custom com at level 0).
Notation "x <= y" := (BLe x y) (in custom com at level 70, no associativity).
Notation "x > y" := (BGt x y) (in custom com at level 70, no associativity).
Notation "x = y" := (BEq x y) (in custom com at level 70, no associativity).
Notation "x <> y" := (BNeq x y) (in custom com at level 70, no associativity).
Notation "x && y" := (BAnd x y) (in custom com at level 80, left associativity).
Notation "'~' b" := (BNot b) (in custom com at level 75, right associativity).
Open Scope com_scope.

Definition W : string := "W".
Definition X : string := "X".
Definition Y : string := "Y".
Definition Z : string := "Z".

Check <{ 3 + (X * 2) }>. (* : aexp *)

Fixpoint aeval (st : state) (a : aexp) : nat :=
  match a with
  | ANum n => n
  | AId x => st x
  | <{a1 + a2}> => (aeval st a1) + (aeval st a2)
  | <{a1 - a2}> => (aeval st a1) - (aeval st a2)
  | <{a1 * a2}> => (aeval st a1) * (aeval st a2)
  end.

Fixpoint beval (st : state) (b : bexp) : bool :=
  match b with
  | <{true}> => true
  | <{false}> => false
  | <{a1 = a2}> => (aeval st a1) =? (aeval st a2)
  | <{a1 <> a2}> => negb ((aeval st a1) =? (aeval st a2))
  | <{a1 <= a2}> => (aeval st a1) <=? (aeval st a2)
  | <{a1 > a2}> => negb ((aeval st a1) <=? (aeval st a2))
  | <{~ b1}> => negb (beval st b1)
  | <{b1 && b2}> => andb (beval st b1) (beval st b2)
  end.

Inductive com : Type :=
  | CSkip
  | CAsgn (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com).

(* Let's define notation *)

Notation "'skip'" :=
         CSkip (in custom com at level 0) : com_scope.
Notation "x := y" :=
         (CAsgn x y)
            (in custom com at level 0, x constr at level 0,
             y at level 85, no associativity) : com_scope.
Notation "x ; y" :=
         (CSeq x y)
           (in custom com at level 90, right associativity) : com_scope.
Notation "'if' x 'then' y 'else' z 'end'" :=
         (CIf x y z)
           (in custom com at level 89, x at level 99,
            y at level 99, z at level 99) : com_scope.
Notation "'while' x 'do' y 'end'" :=
         (CWhile x y)
            (in custom com at level 89, x at level 99, y at level 99) : com_scope.

Definition subtract_slowly_body : com :=
  <{ Z := Z - 1 ;
     X := X - 1 }>.

Definition subtract_slowly : com :=
  <{ while X <> 0 do
       subtract_slowly_body
     end }>.

Fixpoint repl_aexp(a: aexp)(x: string)(e: aexp) : aexp :=
  match a with
  | ANum n => a
  | AId x' => if eqb x x' then e else x'
  | <{a1 + a2}> =>
      let a1' := repl_aexp a1 x e in
      let a2' := repl_aexp a2 x e in
      <{a1' + a2'}>
  | <{a1 - a2}> =>
      let a1' := repl_aexp a1 x e in
      let a2' := repl_aexp a2 x e in
      <{a1' - a2'}>
  | <{a1 * a2}> =>
      let a1' := repl_aexp a1 x e in
      let a2' := repl_aexp a2 x e in
      <{a1' * a2'}>
  end.

Fixpoint repl(a: bexp)(x: string)(e: aexp) : bexp :=
  match a with
  | <{true}> => <{true}>
  | <{false}> => <{false}>
  | <{a1 = a2}> =>
    let a1' := repl_aexp a1 x e in
    let a2' := repl_aexp a2 x e in
      <{a1' = a2'}>
  | <{a1 <> a2}> =>
    let a1' := repl_aexp a1 x e in
    let a2' := repl_aexp a2 x e in
      <{a1' <> a2'}>
  | <{a1 <= a2}> =>
    let a1' := repl_aexp a1 x e in
    let a2' := repl_aexp a2 x e in
      <{a1' <= a2'}>
  | <{a1 > a2}> =>
    let a1' := repl_aexp a1 x e in
    let a2' := repl_aexp a2 x e in
      <{a1' > a2'}>
  | <{~ b1}> =>
    let b1' := repl b1 x e in
      <{~ b1'}>
  | <{b1 && b2}> =>
    let b1' := repl b1 x e in
    let b2' := repl b2 x e in
      <{b1' && b2'}>
  end.

Definition entails(b1 b2: bexp): Prop :=
  forall st, beval st b1 = true -> beval st b2 = true.

Notation " a -.> b " := (entails a b)(at level 40).

Inductive hoare: bexp -> com -> bexp -> Prop :=
  | H_Skip (a: bexp):
    hoare a <{skip}> a
  | H_Assgn (a: bexp)(x: string)(e: aexp):
    hoare (repl a x e) <{ x := e }> a
  | H_Seq (a b c: bexp)(P Q: com):
    hoare a P c -> hoare c Q b ->
    hoare a <{ P ; Q }> b
  | H_If (a g b: bexp)(P Q: com):
    hoare <{ a && g }> P b ->
    hoare <{ a && ~(g)}> Q b ->
    hoare a <{if g then P else Q end}> b
  | H_Conseq (a a' b b': bexp)(P: com):
    a' -.> a ->
    b -.> b' ->
    hoare a P b ->
    hoare a' P b'
  | H_while (a b: bexp)(P: com):
    hoare <{a && b}> P a ->
    hoare a <{ while b do P end }> <{~b && a}>.

Notation " [[ a ]] P [[ b ]] " := (hoare a P b)(at level 40).