I came to this point:
Theorem le_antisymmetric :
antisymmetric le.
Proof.
unfold antisymmetric. intros a b H1 H2. generalize dependent a.
induction b as [|b' IH].
- intros. inversion H1. reflexivity.
- intros.
Output:
b' : nat
IH : forall a : nat, a <= b' -> b' <= a -> a = b'
a : nat
H1 : a <= S b'
H2 : S b' <= a
------------------------------------------------------
a = S b'
My plan was to use transitivity of le:
a <= b -> b <= c -> a <= c
And substitute a := a, b := (S b') and c := a.
So we'll get:
a <= (S b') -> (S b') <= a -> a <= a
I'll use H1 and H2 as 2 hypotheses needed and get Ha: a <= a. Then do an inversion upon it, and get the only way construct this is a = a.
But what syntax should I use to apply transitivity with 2 my hypotheses to get Ha?
Your first induction over b here seems unnecessary. Consider le:
Inductive le (n : nat) : nat -> Prop :=
le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
You should instead be inspecting H1 first. If it's le_n, then that's equality, and you're done. If it's le_S, then presumably that's somehow impossible.
intros a b [ | b' H1] H2.
- reflexivity.
This leaves us with
a, b, b' : nat (* b is extraneous *)
H1 : a <= b'
H2 : S b' <= a
______________________________________(1/1)
a = S b'
Now, transitivity makes sense. It can give you S b' <= b', which is impossible. You can derive a contradiction using induction (I think), or you can use an existing lemma. The whole proof is thus.
intros a b [ | b' H1] H2.
- reflexivity.
- absurd (S b' <= b').
+ apply Nat.nle_succ_diag_l.
+ etransitivity; eassumption.
That last bit is one way to use transitivity. etransitivity turns the goal R x z into R x ?y and R ?y z, for a new existential variable ?y. eassumption then finds assumptions that match that pattern. Here, specifically, you get goals S b' <= ?y and ?y <= b, filled by H2 and H1 respectively. You can also give the intermediate value explicitly, which lets you drop the existential prefix.
transitivity a; assumption.