I'm very new at coq.(I'm reading now Poly section in Software Foundation)
In Basics section, they define ble_nat
function that is x <= y
, then I want to prove transitive law about this, like:
Notation "x =< y" := (ble_nat x y) (at level 50, left associativity) : nat_scope.
Theorem ble_trans: forall (n m o:nat),
n =< m = true -> m =< o = true -> n =< o = true.
Proof.
(* proof *)
But I could not prove this by using simpl
, destruct
, induction
, rewrite
or apply
tactic.
I googled and found out there is already proved library of this, but I could not found out code.
How would I prove this ?
To prove forall (n m : nat), n =< m =true -> exists o, m =< o = true -> n =< o = true
, it is enough to show o := S m
satisfy existential quantifier.
Theorem bleS : forall (n m: nat), n =< m = true -> n =< S m = true.
Proof.
intros n.
induction n.
+ intros m H. reflexivity.
+ intros m H. destruct m.
- simpl in H. discriminate.
- simpl. simpl in H. apply IHn. exact H.
Qed.
Theorem ble_trans_ex: forall (n m :nat),
n =< m = true -> exists o, m =< o = true -> n =< o = true.
Proof.
intros n m H1.
apply ex_intro with (x := S m).
intros H2. apply bleS. exact H1.
Qed.