Как этот код выполняет требуемую функцию?

Question

Lemma odd_pred2n: forall n : nat, Even.odd n -> {p : nat | n = pred (Div2.double p)}. 

Lemma even_2n : forall n, even n -> {p : nat | n = double p}. 

Lemma even_odd_exists_dec:forall n, {p : nat | n = Div2.double p} + {p : nat | n = pred (Div2.double p)}. 
Proof. 
intro n. 
destruct (Even.even_odd_dec n) as [H_parity|H_parity]; 
[ left; apply (Div2.even_2n _ H_parity) 
| right; apply (odd_pred2n _ H_parity)]. 
Defined. 

Definition nat_to_Z_i (n:nat) := 
    match even_odd_exists_dec n with 
    | inl s => let (k, _) := s in Z_of_nat k 
    | inr s => let (k, _) := s in Zopp (Z_of_nat k) 
    end. 

Как это определение определяет инъекцию от nat до Z? И что такое inl, inr и что делает let здесь?

Answer 1

odd_pred2n принимает естественное и доказательство того, что он нечетный, и возвращает преемника половины (округленного вниз), который является нечетным естественным, а также доказательством того, что предшественник двойника является оригинальным странным естественным.

even_2n принимает естественное и доказательство того, что он ровный, и возвращает половину этого даже естественного, а также доказательство того, что двойник является оригинальным даже естественным.

even_odd_exists_dec решает, является ли естественным четность или нечетность, возвращая либо половину, либо преемник половины, а также доказательство того, что двойник или предшественник двойника является оригиналом.

nat_to_Z_i выполняет следующую карту.

0 -> 0 
1 -> - 1 
2 -> 1 
3 -> - 2 
4 -> 2 
5 -> - 3 
6 -> 3 
... 

inl и inr являются конструкторами sum.

Print sum. 

Если s : {x : T | P x}, то s = (x, H) с x : T и H : P x. let (x, y) := z in f x y эквивалентно:

match z with 
| (x, y) => f x y 
end. 

И:

match even_odd_exists_dec n with 
| inl s => let (k, _) := s in Z_of_nat k 
| inr s => let (k, _) := s in Zopp (Z_of_nat k) 
end. 

эквивалентно:

match even_odd_exists_dec n with 
| inl (k, _) => Z_of_nat k 
| inr (k, _) => Zopp (Z_of_nat k) 
end.