Анализ случая Coq и переписывание с функцией, возвращающей типы подмножеств

Я работал над этим простым упражнением о написании сертифицированной функции с использованием типов подмножеств. Идея заключается в том, чтобы сначала написать функцию-предшественникаАнализ случая Coq и переписывание с функцией, возвращающей типы подмножеств

pred : forall (n : {n : nat | n > 0}), {m : nat | S m = n.1}.

, а затем использовать это определение дать FUNTION

pred2 : forall (n : {n : nat | n > 1}), {m : nat | S (S m) = n.1}.

У меня нет никаких проблем с первым. Вот мой код

Program Definition pred (n : {n : nat | n > 0}) : {m : nat | S m = n.1} := 
    match n with 
    | O => _ 
    | S n' => n' 
    end. 
Next Obligation. elimtype False. compute in H. inversion H. Qed.

Но я не могу тренировать второе определение. Я пытаюсь написать эти определения

Program Definition pred2 (n : {n : nat | n > 1}) : {m : nat | S (S m) = n.1} 
:= pred (pred n).

мне удалось доказать два первых обязательство

Next Obligation. apply (gt_trans n 1 0). assumption. auto. Qed. 
Next Obligation. 
    destruct pred. 
    simpl. 
    simpl in e. 
    rewrite <- e in H. 
    apply gt_S_n in H; assumption. 
Qed.

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

Я пробовал следующую тактику безрезультатно.

destruct (pred (n: pred2_obligation_1 (n ; H))). 

destruct (pred (n; pred2_obligation_1 (n ; H))) eqn:?. 
rewrite Heqs.

Я знаю, что могу писать непосредственно с pred2, но идея заключается в том, чтобы использовать и составлять функцию pred.

источник

2015-03-21 Nico Lehmann

Меня интересует множество упражнений, которые у вас есть. Где-то они доступны в Интернете? Можете ли вы опубликовать ссылку или условия поиска Google? – Atsby

Я делаю это упражнение http://www.cis.upenn.edu/~bcpierce/courses/670Fall12/ –

Причина, по которой destruct не имеет никакого эффекта, скорее всего, потому что то, что вы пытаетесь сделать, анализ ситуации не происходит в цели. Неявные аргументы этого термина, вероятно, не соответствуют неявным аргументам термина в цели. В любом случае, вы не можете проводить анализ ситуации на этот срок, не делая цели плохо типизированными.

Но вы можете доказать это обязательство по анализу случая на n.

Next Obligation. 
destruct n. 
inversion H. 
destruct n. 
inversion H. 
subst. 
inversion H1. 
cbn. 
eauto. 
Qed.

Я также смог доказать некоторые вспомогательные теоремы, но я не смог их использовать из-за зависимости типа.

Theorem T1 : forall s1, S (` (pred s1)) = ` s1. 
Proof. intros [[| n1] H1]. inversion H1. cbn. eauto. Qed. 

Theorem T2 : forall T1 (P1 : T1 -> Prop) s1 H1, (forall x1 (H1 H2 : P1 x1), H1 = H2) -> exist P1 (` s1) H1 = s1. 
Proof. intros ? ? [x1 H1] H2 H3. cbn in *. rewrite (H3 _ H1 H2). eauto. Qed.

Я никогда не видел destruct, используемый для функции. Я удивлен, что Coq не жалуется, что эта функция не определяется индуктивно.

источник

2015-03-21 14:58:23

Спасибо, я думаю, что анализ дела на n является лучшим aproach. Однако я до сих пор не понимаю, почему мой подход не работает. Когда вы используете destruct на функции, он анализирует регистр в возвращаемом значении функции. Когда я определяю функцию, используя уточнение «Определение pred2 (n: {n: nat | n> 1}): {m: nat | S (S m) = n.1}. уточнить (((pred ((pred (n.1; _)). 1; _)). 1; _)). " отлично работает –

Вот доказательство, которое я использую. «Уничтожение п применить (gt_trans х 1 0) предположение авто разрушатся п Разрушит пред Симпл Симпл в е перепишет <-........ Е в г применяет gt_S_n в г предположения Разрушит п .... Простой в е0. простой в е. подрефлексивность." –

@NicoLehmann Термин' pred (n; pred2_obligation_1 (n; H)) 'в заключении, а термин' pred (n; pred2_obligation_1 (n; H)) ', который вы пытаетесь уничтожить, отличается. , отключите все обозначения. Термин в заключении включает 'gt', а термин, который вы пытаетесь уничтожить, включает' lt'. В любом случае вы не можете его уничтожить, потому что 'pred2_obligation_2 (n; H)' зависит от это –

Анализ случая Coq и переписывание с функцией, возвращающей типы подмножеств

ответ

Смежные вопросы