Created
August 11, 2025 07:05
-
-
Save mir-ikbch/0152f50c37c14caac7687242c85f011b to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Inductive term := | |
| Tru | |
| | Fls | |
| | IfThenElse : term -> term -> term -> term. | |
| Notation "'If' c1 'Then' c2 'Else' c3" := (IfThenElse c1 c2 c3) | |
| (at level 200, right associativity, format | |
| "'[v ' 'If' c1 '/' '[' 'Then' c2 ']' '/' '[' 'Else' c3 ']' ']'"). | |
| Reserved Notation "x --> y" (at level 60). | |
| Inductive step : term -> term -> Prop := | |
| EIfTrue : forall t2 t3, (If Tru Then t2 Else t3) --> t2 | |
| | EIfFalse : forall t2 t3, (If Fls Then t2 Else t3) --> t3 | |
| | EIf : forall t1 t1' t2 t3, t1 --> t1' -> (If t1 Then t2 Else t3) --> (If t1' Then t2 Else t3) | |
| where "x --> y" := (step x y). | |
| Ltac auto_inversion step := | |
| repeat match goal with | |
| H : step Tru _ |- _ => inversion H | |
| | H : step Fls _ |- _ => inversion H | |
| | H : step (IfThenElse _ _ _) _ |- _ => inversion H; clear H; subst; try f_equal; auto | |
| end. | |
| Theorem step_deterministic : forall t t', t --> t' -> forall t'', t --> t'' -> t' = t''. | |
| Proof. | |
| intros t t' H. | |
| induction H; intros; auto_inversion step. | |
| (* ^ - ^ *) | |
| Qed. | |
| Reserved Notation "x -->' y" (at level 60). | |
| Inductive step' : term -> term -> Prop := | |
| EIfTrue' : forall t2 t3, (If Tru Then t2 Else t3) -->' t2 | |
| | EIfFalse' : forall t2 t3, (If Fls Then t2 Else t3) -->' t3 | |
| | EIf' : forall t1 t1' t2 t3, t1 -->' t1' -> (If t1 Then t2 Else t3) -->' (If t1' Then t2 Else t3) | |
| | EFunny2 : forall t1 t2 t2' t3, t2 -->' t2' -> (If t1 Then t2 Else t3) -->' (If t1 Then t2' Else t3) | |
| where "x -->' y" := (step' x y). | |
| Ltac fo := eexists; firstorder (try constructor; eauto). | |
| Lemma step'_loc_conf : forall t s s', | |
| t -->' s -> t -->' s' -> | |
| exists u, (s = u /\ s' = u) \/ (s = u /\ s' -->' u) \/ (s -->' u /\ s' = u) \/ (s -->' u /\ s' -->' u). | |
| Proof. | |
| intros t s s' H. | |
| revert s'. | |
| induction H; intros; auto_inversion step'; try solve [fo]. | |
| - destruct (IHstep' _ H5). | |
| destruct H0 as [|[|[]]]; destruct H0; subst; fo. | |
| - destruct (IHstep' _ H5). | |
| destruct H0 as [|[|[]]]; destruct H0; subst; fo. | |
| (* ^ o ^ *) | |
| Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment