Rel chapter from Logical foundations. I was given a solution to the excersize that I'm trying to comprehend:
Definition antisymmetric {X: Type} (R: relation X) :=
forall a b : X, (R a b) -> (R b a) -> a = b.
Theorem le_antisymmetric :
antisymmetric le.
Proof.
unfold antisymmetric. intros a b [| b' H1] H2.
- reflexivity.
- absurd (S b' <= b').
+ apply le_Sn_n.
+ etransitivity ; eassumption.
I don't understand, how does intro pattern [| b' H1] work? After intros it shows:
2 subgoals (ID 43)
a, b : nat
H2 : a <= a
============================
a = a
subgoal 2 (ID 46) is:
a = S b'
2-nd subgoal:
a, b, b' : nat
H1 : a <= b'
H2 : S b' <= a
============================
a = S b'
I understand that it is equivalent to destruct, but what sort of destruct? It's definitely not a simple destruct b.
Also I'm trying to understand the logics behind using absurd (S b' <= b') tactics. Does it mean that if we prove that a = S b' in this context, it would imply that after we rewrite a to S b' in H1, we get: S b' <= b', which is a universally false statement (absurd)?
intros a b [| b' H1] H2 is equivalent to
intros a b H H2.
destruct H as [| b' H1].
destruct patterns generally follow the rules that if an inductive type has a single constructor (e.g. products) then for x in that inductive type, destruct x as [a b c...] does (non-recursive) induction and renames the new variables to a, b, c, etc. When the inductive type has more than one constructor, there are multiple cases. For that, you use destruct x as [a b c ... | d e f ... | ...]. These destruction patterns can be nested if needed, e.g. destruct x as [[a b] | [c [d | e]]]. Note that if a constructor takes no arguments, there is nothing to rename, so you can leave the pattern empty.
In particular, something like a natural number can be destructed with destruct n as [ | n']. This divides into the cases where n is zero (and the constructor has no arguments, so there's nothing to the left of the |) or n is the successor of n'. Similarly, a list could be destructed as destruct li as [ | a li'] to divide into the cases where the list is nil and where it is cons a li'. The space to the left of the | is unnecessary, so you could do destruct li as [| a li'].
What's happening in your case specifically is that le is defined as an inductive type something along the lines of
Inductive le (n : nat) : nat -> Prop :=
| le_n : le n n
| le_S : forall m : nat, le n m -> le n (S m).
So there are two cases: one with no arguments, and the successor case where the arguments are m: nat and H: le n m. Hence, the destruct pattern is [| m H].
To answer your second question, absurd (S b' <= b'). means that (we think) we're able to prove S b' <= b' in the current context. We can also prove (in the same context) that S b' <= b' is absurd, i.e. leads to a witness of False (more precisely, S b' <= b' -> False). Using the induction principle for False, this allows us to generate a witness for any type, and in particular for a = S b'.
You can see what kind of proof term absurd produces with a minimal experiment.
Goal forall A B: Type, A.
Proof.
intros A B.
absurd B.
Show Proof.
This should print (fun A B : Type => False_rect A (?Goal ?Goal0)). The first goal (?Goal) has type ~B (i.e. B -> False). The second goal (?Goal0) has type B. If we can provide both, then ?Goal ?Goal0 has type False, so False_rect A (?Goal ?Goal0) produces a witness of type A.