Require Arith.
Rewriting with Equality |
|
One of the most basic things to do is to use a
proof of equality in equational reasoning, substituting
equals for equals.
This is easy to do with tactics using the rewrite -> H. command, where H is something
of type (x=y). How do we do this by hand?
|
Print eq_rect.
Recall the definition of equality (you can say What this means is that the equality is the smallest relation which, for some fixed X of type A has the proof that x = x (note that X=X is the short for Eq A X X).
The elimination for the equality looks something like this:
|
Print eq_rect.
Section Example1.
Definition P (n:nat) := (1<=n).
Variable a : nat.
Lemma pf1: 1 <= 2. eauto. Qed.
Print pf1.
Check refl_equal 2.
Check (eq_rect 2 P pf1 (1+1) ).
End Example1.
|
Section Rewriting.
Variable A: Set.
Variable x : A.
Variable y: A.
Variable p : (x=y).
Variable f : A -> Set.
Variable g : A * A -> Set.
Definition r1 (i : (f x)) : (f y) :=
match p in ( _ = x0) return (f x0) with
refl_equal => i end.
Definition r2 (i : (g (pair x x))) : (g (pair y y)) :=
match p in ( _ = x0) return (g (pair x0 x0)) with
refl_equal => i end.
End Rewriting.
You might also want to compare r1 and r2.
|
Lists with length |
| In class, we started defining lists with length in Coq. |
Inductive List (A:Set) : nat -> Set :=
| Nil : List A 0
| Cons : forall (m:nat), (A -> (List A m) -> (List A (S m))).
Check List_rec.
Check (List_rec nat (fun n :nat => fun _ => nat)).
Definition sum := List_rec nat (fun x:nat => fun _ => nat)
0 (fun len_rest => fun elem => fun _ => fun rest_sum => (elem+rest_sum)).
Check (Cons nat 1 10 (Cons nat 0 20 (Nil nat))).
Eval compute in (sum 2 ((Cons nat 1 10 (Cons nat 0 20 (Nil nat))))).
Print List_ind.
Print List_rect.
Fixpoint sum_2 (n:nat) (l:(List nat n)) {struct l} : nat :=
match l with
| Nil => 0
| Cons m a xs => a + (sum_2 m xs)
end.
Print List_rect.
Check Cons.
Check (Cons bool 0 true (Nil bool)).
To be a 2? |
| Let us define a simple inductive predicate that tells us that a number is 2. |
Inductive isTwo : nat -> Prop := TwoProof : isTwo 2.
Check TwoProof.
So, isTwo n is a Prop type for any natural number n.
There is one introduction rule for isTwo, called TwoProof
which is a proof of isTwo 2.
|
| Now we can prove that if we have a proof that 2=x then (isTwo x), for any x. |
Definition two_is_two (x:nat) (p : (2=x)) : isTwo x :=
match p in (_ = x) return (isTwo x) with
| refl_equal => TwoProof end.
Definition and_only_two (x:nat) (P : isTwo x) : (2=x) :=
match P in (isTwo n) return (2=n) with
| TwoProof => refl_equal 2 end .
So, with the above we have shown that if and only if x=2 then isTwo x,
which seems pretty sensible.
|
How does the two_is_two above work?
|
| First, we take apart the proof p of type 2=x. The "in" part renames the x as y, and instructs as that we will return (isTwo y). When pathing refl_equal the y will be substituted with 2 (i.e., in the branch it will be definitionally equal to 2), so TwoProof will have the type (isTwo y) (since 2 := y). |
|
Suppose we want to prove that 1 is not two. Here's a lemma:
Remember that ~P is defined as P -> False.
|
Definition one_not_two (H : isTwo 1) : False := sym_not_eq (n_Sn 1) (and_only_two 1 H).
Check (sym_not_eq (n_Sn 1)).
Above we use a convenient little lemma that says:
(n_Sn 1) : ~(1=2). From that we apply another lemma called sym_not_eq
that says if ~(x=y) then ~(y=x). This gives us something of the type
(sym_not_eq (n_Sn 1)) (~(2=1)).
Recall, that since we have an assumption H : isTwo 1, we can
use the lemma and_only_two to obtain the proof and_only_two 1 H of type (2=1). Giving
this proof to sym_not_eq (n_Sn 1) gives us False, thus proving the negation.
|
Another Example |
| How to construct a proof of (y=x) from (x=y)? |
Lemma symmetry_with_tact (A:Set) (x y:A) (p:(x=y)) : (y=x).
intros.
symmetry. eapply p. Qed.
|
| Now, that we have symmetry, we can try this proof, where we have (n=2) instead (2=n). We can use symmetry, defined above, and proceed as before. |
Definition example3 : forall n, (n=2) -> isTwo n :=
fun n => fun p =>
match (symmetry_with_tact nat n 2 p) in ( _ = n2) return isTwo n2 with
refl_equal => TwoProof
end.
Some simple proofs about arithmetic and addition |
| Implementation with tactics: |
Lemma plus_z_thm : forall n, n=(n+0).
fix 1.
intros.
destruct n.
refine (refl_equal _ ).
simpl. rewrite <- (plus_z_thm n).
refine (refl_equal _). Qed.
| Direct implementation of the proof as a fixpoint: |
Fixpoint plus_z_thm_d (n:nat) : n=n+0 :=
match n as n0 return (n0=n0+0) with
| 0 => refl_equal 0
| S n' =>
(eq_ind n' (fun n1 => S n' = S n1) (refl_equal (S n')) (n'+0) (plus_z_thm_d n'))
end.
Section EI.
Check eq_ind.
Variable A: Type. Variable x y: A. Variable P : A -> Prop.
Variable q : (P x). Variable z : (x=y).
Eval unfold eq_ind eq_rect in @eq_ind A x P.
|
In general if you know that (x=y) and you want to rewrite some type P x with Py, you must do the following.
1. Figure out a function P : A -> Prop such that (P x) = Px.
Then take an (f : P x) and produce a P y by
matching on the proof
[
fun (f : P x) (y : A) (e : x = y) =>
match e in (_ = y0) return (P y0) with
| refl_equal => f
end
: P x -> forall y : A, x = y -> P y
]
|
End EI.
Lemma succ_comm : forall n, (S n) = n+1.
fix 1.
intros.
destruct n.
cases on n
|
| case n=0 |
reflexivity.
| case n=S n |
simpl. rewrite <- (succ_comm n). reflexivity. Qed.
Print succ_comm.
succ_comm_d is the same function implemented directly without tactics.
|
Fixpoint succ_comm_d (n:nat) : (S n) = n+1 :=
match n as n0 return (S n0 = n0 + 1) with
| O => refl_equal (0 + 1)
| S n0 =>
eq_ind (S n0) (fun n1 => S (S n0) = S n1)
(refl_equal (S (S n0))) (n0 + 1) (succ_comm_d n0)
end.
Print eq_rect.
Lemma succ_comm2 : forall m n, m + (S n) = S ( m+n).
induction m. intros. reflexivity.
intros n. simpl; rewrite -> IHm. reflexivity. Qed.
|
Lemma assoc_plus : forall a b c, (a+b)+c = a + (b + c).
fix 1. intros.
destruct a.
reflexivity.
intros. simpl. rewrite -> (assoc_plus a b c). reflexivity. Qed.
Print assoc_plus.
Lemma comm_plus:forall (m n : nat), (m+n)=(n+m).
induction m.
intros. simpl. apply ( plus_z_thm n).
cut (forall m n, n + (S m) = S (n+m)).
intros. simpl. rewrite -> IHm. rewrite <- H. reflexivity.
induction n. simpl. eauto.
simpl. rewrite -> IHn. reflexivity. Qed.
Lemma symm_eq : forall A, forall (x y: A), (x=y) -> (y=x). eauto. Qed.
Lemma trans_eq : forall A, forall (x y z : A), (x = y) /\ (y =z) -> (x=z).
intros. destruct H. rewrite -> H. rewrite -> H0. reflexivity. Qed.
Formalizing less-then predicate |
Proposition le_e x y which means that x is less than y.
How do we arrive at this definition?
|
|
What do proofs that one natural number is less than another look like?
We use an inductive definition below to represent such proof terms. |
Inductive le_e : nat -> nat -> Prop :=
| le_e_z : forall m, (le_e 0 (S m))
| le_e_s : forall a b, (le_e a b) -> (le_e (S a) (S b)).
Derive Inversion le_inversion_lemma with (forall (x:nat) (y:nat), (le_e x y)) Sort Prop.
Check le_inversion_lemma.
| The above definition states that (le_e m n) is the smallest set such that 0<(S m) and if (a<b) then (S a) < (S b). |
| Now, we can assure ourselves of some propseties of the less-then as we have defined it. |
Lemma not_con : forall m n, ~(le_e m n) -> ~(le_e (S m) (S n)).
induction m.
intros. unfold not ; intros. inversion H0. subst. eapply H. eapply H3.
intros. unfold not; intros. inversion H0. subst. eapply H. eapply H3. Qed.
The relation le_e is irreflexive:
|
Lemma irr : forall n, ~(le_e n n).
fix 1. destruct n.
| Case 0 |
intro absurd.
inversion absurd.
intro absurd.
inversion absurd. (eapply (irr n)). eapply H1. Qed.
Print irr.
The relation le_e is antysymmetric:
|
Lemma anty_simm_le : forall m n, le_e m n -> ~(le_e n m).
induction m.
intros. unfold not; intros. inversion H0.
intros. destruct n. inversion H. eapply not_con. eapply IHm. inversion H. subst; eauto. Qed.
The relation le_e is transitive:
|
Lemma trans_le : forall m n p, (le_e m n) -> (le_e n p) -> (le_e m p).
induction m.
intros. destruct n. inversion H. inversion H0. subst. constructor.
intros.
inversion H. subst. inversion H0. subst. constructor. eapply IHm. eauto. eauto. Qed.
The relation le_e is asymetric:
|
Lemma asymetry_le : forall m n, (m <> n) /\ (le_e m n) -> ~(le_e n m).
induction m.
intros.
destruct H. unfold not. intros. inversion H1.
intros. destruct H. unfold not. intros. unfold not in IHm. inversion H1. subst. inversion H0.
subst. eapply IHm with a. constructor. injection. intros. subst. eapply H. reflexivity. inversion H0. subst; eauto. eauto. Qed.
Lemma plus_le_e : forall m n p, (le_e m n) -> (le_e (p+m) (p+n)).
fix 3. intros. destruct p. apply H.
simpl; eapply le_e_s. eapply (plus_le_e ). eapply H. Qed.
Lemma minus_le_e : forall m n p, (le_e p m) -> (le_e p n) -> (le_e n m) -> (le_e (n-p) (m-p)).
induction m.
intros.
inversion H1.
intros.
inversion H. simpl. subst. destruct n. constructor. simpl. eauto. subst.
destruct n. Focus 2. simpl. eapply IHm. eauto. inversion H0; eauto. inversion H1. eauto.
inversion H0. Qed.
Print plus_le_e.
Fixpoint is_less (m n:nat) {struct m} : bool :=
match m with
| 0 => (match n with 0 => false | S _ => true end)
| S x => (match n with 0 => false | S y => is_less x y end)
end.
Lemma forward_less : forall m n, (le_e m n) -> (is_less m n = true).
induction m.
intros. destruct n. inversion H. simpl. reflexivity.
intros. destruct n. inversion H. simpl. eapply IHm. inversion H; eauto. Qed.
Lemma back_less : forall m n, (is_less m n = true) -> (le_e m n).
induction m.
intros. destruct n. simpl in *|-*. inversion H.
constructor.
intros. destruct n. simpl in H. inversion H. simpl in *|-*. constructor. eapply IHm. eapply H. Qed.
Lemma qwe : forall m n, if (is_less m n) then (le_e m n) else ~(le_e m n).
induction m.
intros. destruct n. simpl. intro; inversion H. simpl. constructor.
intros. destruct n. simpl. intro; inversion H. simpl.
assert (Q:= (IHm n)).
destruct (is_less m n).
constructor; eapply Q. intro. eapply Q. inversion H. subst; eauto. Qed.
Lemma example_existential: forall m n, (le_e m n) -> { x : nat | x + m = n }.
induction m.
intros. exists n. eauto. intros.
destruct n. exists 4. inversion H.
cut (le_e m n). intros. assert (Q:= IHm n H0).
destruct Q. exists ( x). rewrite <- e. eauto. inversion H; subst; trivial. Qed.
A Simple Language example |
Inductive Expr : Set :=
| Const : nat -> Expr
| Plus : Expr -> Expr -> Expr
| If1 : Expr -> Expr -> Expr -> Expr
| Eq : Expr -> Expr -> Expr.
Inductive isValue : Expr -> Prop := IsValue : forall n, isValue (Const n).
Inductive Red : Expr -> Expr -> Prop :=
| Red_Plus : forall m n, Red (Plus (Const m) (Const n)) (Const (m+n))
| Red_Eq_T : forall m, Red (Eq (Const m) (Const m)) (Const 1)
| Red_Eq_F : forall m n, ~(m=n) -> Red (Eq (Const m) (Const n)) (Const 0)
| Red_Eq_IfTrue : forall e1 e2, Red (If1 (Const 1) e1 e2) e1
| Red_Eq_IfFalse : forall e1 e2, Red (If1 (Const 0) e1 e2) e2.
Inductive RedC : Expr -> Expr -> Prop :=
| REDEX : forall e1 e2, Red e1 e2 -> RedC e1 e2
| Red_PlusC1 : forall e1 e2 e3, (RedC e1 e2) -> (RedC (Plus e1 e3) (Plus e2 e3))
| Red_PlusC2 : forall e1 e2 e3, (isValue e1) -> (RedC e2 e3) -> (RedC (Plus e1 e2) (Plus e1 e3))
| Red_EqC1 : forall e1 e2 e3, (RedC e1 e2) -> (RedC (Eq e1 e3) (Eq e2 e3))
| Red_EqC2 : forall e1 e2 e3, (isValue e1) -> (RedC e2 e3) -> (RedC (Eq e1 e2) (Eq e1 e3))
| Red_If1 : forall e1 e2 e3 e4, (RedC e1 e2) -> (RedC (If1 e1 e3 e4) (If1 e2 e3 e4)).
Hint Constructors Red RedC.
Lemma no_value : forall e, isValue e -> ~ ex (fun f : Expr => RedC e f).
induction e. intros. intro. destruct H0. inversion H0. subst. inversion H1.
intros. inversion H. intros; inversion H. intros; inversion H. Qed.
Inductive num_or_error : Set :=
| R : nat -> num_or_error
| ERR : num_or_error.
Definition lift f e1 e2 :=
match e1 with
| ERR => ERR
| R x => (match e2 with ERR => ERR | R y => R (f x y) end) end.
Fixpoint eq (m n : nat) {struct m} : nat :=
match m with 0 => (match n with 0 => 1 | _ => 0 end)
| S m => (match n with 0 => 0 | S n => eq m n end) end.
Fixpoint eval (e: Expr) {struct e} : num_or_error :=
match e with
| Plus e1 e2 => lift plus (eval e1) (eval e2)
| Eq e1 e2 => lift (eq) (eval e1) (eval e2)
| If1 e1 e2 e3 => (match eval e1 with ERR => ERR | R 1 => (eval e2) | R _ => (eval e3) end)
| Const n => R n
end.
Lemma ee: forall m, (eq m m) = 1.
induction m. eauto. eauto. Qed.
Hint Resolve ee.
Lemma ee2 : forall m n, m<>n -> (eq m n) = 0.
induction m. intros. destruct n. simpl. absurd (0<>0). eauto. eauto. eauto.
intros. destruct n. simpl. eauto. simpl. eapply IHm. eauto. Qed.
Lemma red_preserv: forall e1 e2, (Red e1 e2) -> (eval e1) = (eval e2).
induction e1.
intros. inversion H.
intros. simpl in *|-*. inversion H. subst. simpl. reflexivity.
intros. inversion H. subst. simpl. reflexivity. subst. simpl. reflexivity.
intros. inversion H. subst. simpl. rewrite -> ee. reflexivity.
subst. inversion H. subst. simpl. cutrewrite ((eq m n) = 0). reflexivity. eapply ee2. eauto. Qed.
Lemma redC_preserv: forall e1 e2, (RedC e1 e2) -> (eval e1) = (eval e2).
intros. induction H. eapply red_preserv. eauto.
(simpl; rewrite -> IHRedC; reflexivity).
simpl. rewrite -> IHRedC. reflexivity.
simpl. rewrite -> IHRedC. reflexivity.
simpl. rewrite -> IHRedC. reflexivity.
simpl. rewrite -> IHRedC. reflexivity.
Qed.
Inductive RTC : Expr -> Expr -> Prop :=
| Refl_R : forall e, RTC e e
| Step_R : forall e1 e2 e3, (RedC e1 e2) -> (RTC e2 e3) -> (RTC e1 e3).
Hint Constructors RTC.
Lemma rtc_split : forall e1 e2, (RTC e1 e2) -> (exists e, (RTC e1 e) /\ (RTC e e2)).
intros.
induction H.
exists e. eauto.
destruct IHRTC.
exists e3. eauto. Qed.
Print rtc_split.
Lemma RTC_preserv : forall e1 e2, (RTC e1 e2) -> (eval e1) = (eval e2).
intros.
induction H. reflexivity.
rewrite <- IHRTC.
eapply redC_preserv. eauto. Qed.
Functional Scheme eval_ind := Induction for eval.
Trees |
Section Trees.
Variable A : Set.
Inductive tree (A:Set): Set :=
| Tip : tree A
| Node : tree A -> A -> tree A ->tree A.
Require Export Max.
Check max.
Fixpoint height (t:tree A) {struct t} : nat :=
match t with
| Tip => 0
| Node a _ b => S (max (height a) (height b)) end.
Fixpoint size (t:tree A) {struct t} : nat :=
match t with
| Tip => 0
| Node a _ b => S ((size a) + (size b))
end.
End Trees.
| Height vs. size |
Lemma exdample1 : forall A, forall t: tree A, (height A t) <= (size A t).
intros. induction t. eauto. simpl. eapply Le.le_n_S.
cut ((height A t1) <= (height A t2) \/ (height A t2) <= (height A t1)). intros.
destruct H. cutrewrite (max (height A t1) (height A t2) = (height A t2)). eapply Le.le_trans with (size A t2). eauto.
eapply Le.le_trans with (size A t2). eauto. cutrewrite ( (size A t1 + size A t2) = (size A t2 + size A t1)). eauto with arith. eauto with arith.
eauto with arith.
cutrewrite (max (height A t1) (height A t2) = (height A t1)). eauto with arith. eauto with arith.
compare (height A t1) (height A t2). intros. rewrite -> e. eauto.
intros. assert (X:= Coq.Arith.Compare_dec.lt_eq_lt_dec (height A t1) (height A t2)).
destruct X. destruct s. eauto with arith. destruct (n e). eapply or_intror. eauto with arith. Qed.
Derive Inversion tree_inv with (forall A, tree A).
Check tree_inv.
Print tree_inv.
Inductive HTree (A:Set) : nat -> Set :=
| H_Tip : HTree A 0
| H_Node : forall lh rh, (HTree A lh) -> A -> (HTree A rh) -> (HTree A (S (max lh rh))).
Derive Inversion htree_inv with (forall A:Set, forall m:nat, (HTree A m)).
Check htree_inv.
Definition t_to_t (A:Set) (x:tree A) : (HTree A (height A x)).
induction x.
simpl. constructor.
simpl. constructor. eauto. eauto. eauto. Qed.